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-ran8x32.opb
MD5SUM	ff0017de67077abd1f68238274b64e50
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1695644
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1517603678
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	1517603678
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.03
Number of variables	5376
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	640
Trace number 14765

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        809288 kB
Buffers:         31652 kB
Cached:         170784 kB
SwapCached:          0 kB
Active:          13592 kB
Inactive:       191652 kB
HighTotal:      131008 kB
HighFree:        30884 kB
LowTotal:       903652 kB
LowFree:        778404 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14452 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:34:35 (client local time) WITH STATUS 10 IN 1200.14 SECONDS
stats: 19368 7 1200.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> Adder-cost: 646   maxlim: 45920   bits: 16/16
c ---[ 332]---> Adder-cost: 670   maxlim: 69856   bits: 17/17
c ---[ 330]---> Adder-cost: 670   maxlim: 67552   bits: 17/17
c ---[ 328]---> Adder-cost: 670   maxlim: 71392   bits: 17/17
c ---[ 326]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 324]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 322]---> Adder-cost: 670   maxlim: 70368   bits: 17/17
c ---[ 320]---> Adder-cost: 670   maxlim: 64608   bits: 17/16
c ---[ 318]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost:  919     Base: 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 294]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 286]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 284]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 282]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 280]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 278]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1661     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 274]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 272]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 1187     Base: 2 2 2 2 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2
c ---[ 260]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 258]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 256]---> Sorter-cost: 1321     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:   10
c ---[ 254]---> BDD-cost:   15
c ---[ 253]---> BDD-cost:   12
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   10
c ---[ 249]---> BDD-cost:   16
c ---[ 248]---> BDD-cost:   14
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:   12
c ---[ 245]---> BDD-cost:   16
c ---[ 244]---> BDD-cost:   16
c ---[ 243]---> BDD-cost:   15
c ---[ 242]---> BDD-cost:   15
c ---[ 241]---> BDD-cost:   12
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   14
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:   11
c ---[ 235]---> BDD-cost:   11
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   17
c ---[ 231]---> BDD-cost:   15
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:   12
c ---[ 227]---> BDD-cost:   12
c ---[ 226]---> BDD-cost:   18
c ---[ 225]---> BDD-cost:   15
c ---[ 224]---> BDD-cost:   15
c ---[ 223]---> BDD-cost:   15
c ---[ 222]---> BDD-cost:   10
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:   15
c ---[ 219]---> BDD-cost:   17
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   16
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   10
c ---[ 214]---> BDD-cost:   16
c ---[ 213]---> BDD-cost:   14
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:   12
c ---[ 210]---> BDD-cost:   17
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   16
c ---[ 207]---> BDD-cost:   15
c ---[ 206]---> BDD-cost:   12
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:   16
c ---[ 201]---> BDD-cost:   11
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   13
c ---[ 196]---> BDD-cost:   17
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   10
c ---[ 193]---> BDD-cost:   12
c ---[ 192]---> BDD-cost:   12
c ---[ 191]---> BDD-cost:   18
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:   15
c ---[ 188]---> BDD-cost:   15
c ---[ 187]---> BDD-cost:   14
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   15
c ---[ 184]---> BDD-cost:   17
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:   16
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   10
c ---[ 179]---> BDD-cost:   16
c ---[ 178]---> BDD-cost:   14
c ---[ 177]---> BDD-cost:   15
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   16
c ---[ 172]---> BDD-cost:   15
c ---[ 171]---> BDD-cost:   12
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   14
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:   11
c ---[ 165]---> BDD-cost:   15
c ---[ 164]---> BDD-cost:   11
c ---[ 163]---> BDD-cost:   13
c ---[ 162]---> BDD-cost:   13
c ---[ 161]---> BDD-cost:   17
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:   12
c ---[ 157]---> BDD-cost:   12
c ---[ 156]---> BDD-cost:   18
c ---[ 155]---> BDD-cost:   15
c ---[ 154]---> BDD-cost:   11
c ---[ 153]---> BDD-cost:   15
c ---[ 152]---> BDD-cost:   15
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   15
c ---[ 149]---> BDD-cost:   17
c ---[ 148]---> BDD-cost:   11
c ---[ 147]---> BDD-cost:   16
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   16
c ---[ 143]---> BDD-cost:   15
c ---[ 142]---> BDD-cost:   11
c ---[ 141]---> BDD-cost:   14
c ---[ 140]---> BDD-cost:   15
c ---[ 139]---> BDD-cost:   12
c ---[ 138]---> BDD-cost:   19
c ---[ 137]---> BDD-cost:   16
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   14
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   16
c ---[ 129]---> BDD-cost:   11
c ---[ 128]---> BDD-cost:   11
c ---[ 127]---> BDD-cost:   13
c ---[ 126]---> BDD-cost:   13
c ---[ 125]---> BDD-cost:   17
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   10
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   12
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   18
c ---[ 118]---> BDD-cost:   15
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   10
c ---[ 114]---> BDD-cost:   15
c ---[ 113]---> BDD-cost:   17
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   15
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:   15
c ---[ 104]---> BDD-cost:   12
c ---[ 103]---> BDD-cost:   19
c ---[ 102]---> BDD-cost:   16
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   12
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   14
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:   11
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   13
c ---[  91]---> BDD-cost:   13
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   15
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   12
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   18
c ---[  83]---> BDD-cost:   15
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   15
c ---[  80]---> BDD-cost:   12
c ---[  79]---> BDD-cost:   12
c ---[  78]---> BDD-cost:   15
c ---[  77]---> BDD-cost:   15
c ---[  76]---> BDD-cost:   11
c ---[  75]---> BDD-cost:   15
c ---[  74]---> BDD-cost:   15
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   15
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   11
c ---[  69]---> BDD-cost:   16
c ---[  68]---> BDD-cost:   13
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   16
c ---[  65]---> BDD-cost:   15
c ---[  64]---> BDD-cost:   14
c ---[  63]---> BDD-cost:   15
c ---[  62]---> BDD-cost:   12
c ---[  61]---> BDD-cost:   19
c ---[  60]---> BDD-cost:   16
c ---[  59]---> BDD-cost:   15
c ---[  58]---> BDD-cost:   12
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   16
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   11
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   15
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   12
c ---[  44]---> BDD-cost:   12
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   18
c ---[  41]---> BDD-cost:   15
c ---[  40]---> BDD-cost:   15
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   15
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   11
c ---[  34]---> BDD-cost:   16
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   15
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   16
c ---[  29]---> BDD-cost:   14
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   12
c ---[  26]---> BDD-cost:   19
c ---[  25]---> BDD-cost:   16
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   14
c ---[  20]---> BDD-cost:   14
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:   16
c ---[  17]---> BDD-cost:   11
c ---[  16]---> BDD-cost:   11
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   17
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   15
c ---[   9]---> BDD-cost:   12
c ---[   8]---> BDD-cost:   12
c ---[   7]---> BDD-cost:   18
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   15
c ---[   4]---> BDD-cost:   15
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  148605   395321 |   44581       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/42797          
c   -- var.elim.:  2000/42797          
c   -- var.elim.:  3000/42797          
c   -- var.elim.:  4000/42797          
c   -- var.elim.:  5000/42797          
c   -- var.elim.:  6000/42797          
c   -- var.elim.:  7000/42797          
c   -- var.elim.:  8000/42797          
c   -- var.elim.:  9000/42797          
c   -- var.elim.:  10000/42797          
c   -- var.elim.:  11000/42797          
c   -- var.elim.:  12000/42797          
c   -- var.elim.:  13000/42797          
c   -- var.elim.:  14000/42797          
c   -- var.elim.:  15000/42797          
c   -- var.elim.:  16000/42797          
c   -- var.elim.:  17000/42797          
c   -- var.elim.:  18000/42797          
c   -- var.elim.:  19000/42797          
c   -- var.elim.:  20000/42797          
c   -- var.elim.:  21000/42797          
c   -- var.elim.:  22000/42797          
c   -- var.elim.:  23000/42797          
c   -- var.elim.:  24000/42797          
c   -- var.elim.:  25000/42797          
c   -- var.elim.:  26000/42797          
c   -- var.elim.:  27000/42797          
c   -- var.elim.:  28000/42797          
c   -- var.elim.:  29000/42797          
c   -- var.elim.:  30000/42797          
c   -- var.elim.:  31000/42797          
c   -- var.elim.:  32000/42797          
c   -- var.elim.:  33000/42797          
c   -- var.elim.:  34000/42797          
c   -- var.elim.:  35000/42797          
c   -- var.elim.:  36000/42797          
c   -- var.elim.:  37000/42797          
c   -- var.elim.:  38000/42797          
c   -- var.elim.:  39000/42797          
c   -- var.elim.:  40000/42797          
c   -- var.elim.:  41000/42797          
c   -- var.elim.:  42000/42797          
c   -- var.elim.:  42797/42797          
c   -- var.elim.:  1000/22516          
c   -- var.elim.:  2000/22516          
c   -- var.elim.:  3000/22516          
c   -- var.elim.:  4000/22516          
c   -- var.elim.:  5000/22516          
c   -- var.elim.:  6000/22516          
c   -- var.elim.:  7000/22516          
c   -- var.elim.:  8000/22516          
c   -- var.elim.:  9000/22516          
c   -- var.elim.:  10000/22516          
c   -- var.elim.:  11000/22516          
c   -- var.elim.:  12000/22516          
c   -- var.elim.:  13000/22516          
c   -- var.elim.:  14000/22516          
c   -- var.elim.:  15000/22516          
c   -- var.elim.:  16000/22516          
c   -- var.elim.:  17000/22516          
c   -- var.elim.:  18000/22516          
c   -- var.elim.:  19000/22516          
c   -- var.elim.:  20000/22516          
c   -- var.elim.:  21000/22516          
c   -- var.elim.:  22000/22516          
c   -- var.elim.:  22516/22516          
c   -- var.elim.:  137/137          
c   -- subsuming                       
c   -- var.elim.:  1000/2697          
c   -- var.elim.:  2000/2697          
c   -- var.elim.:  2697/2697          
c   -- var.elim.:  1000/2236          
c   -- var.elim.:  2000/2236          
c   -- var.elim.:  2236/2236          
c   -- var.elim.:  315/315          
c   -- subsuming                       
c   -- var.elim.:  960/960          
c   -- var.elim.:  178/178          
c   -- var.elim.:  30/30          
c   -- subsuming                       
c   -- var.elim.:  40/40          
c   -- var.elim.:  82/82          
c |         0 |  131115   408832 |      --       0       --      -- |     --   | -13048/27006
c |         0 |  131115   408832 |   52446       0        0     nan |  0.000 % |
c |       100 |  131014   408482 |   57646      97      356     3.7 | 14.406 % |
c |       250 |  130897   408056 |   63354     243     1066     4.4 | 14.460 % |
c |       476 |  130870   407920 |   69675     467     2136     4.6 | 14.470 % |
c |       813 |  130644   407119 |   76510     775     3443     4.4 | 14.585 % |
c |      1320 |  130501   406623 |   84069    1272     5820     4.6 | 14.652 % |
c |      2080 |  130309   405966 |   92340    2014     9196     4.6 | 14.742 % |
c |      3219 |  130132   405326 |  101436    3140    14654     4.7 | 14.828 % |
c |      4927 |  130030   404986 |  111492    4841    23514     4.9 | 14.882 % |
c |      7489 |  129665   403676 |  122297    7376    38994     5.3 | 15.061 % |
c |     11333 |  128446   399383 |  133262   11111    57691     5.2 | 15.693 % |
c |     17099 |  127096   394853 |  145047   16772    86852     5.2 | 16.428 % |
c |     25751 |  126139   391617 |  158351   25297   183344     7.2 | 16.923 % |
c |     38728 |  124995   387833 |  172606   38143   320176     8.4 | 17.549 % |
c ==============================================================================
c (current CPU-time: 120.64 s)
c ==============================================================================
c [1mFound solution: 5548679[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10869   maxlim: 3357655   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     57653 |  199076   653154 |   59722   56767   486705     8.6 | 17.549 % |
c   -- subsuming                       
c   -- var.elim.:  1000/16002          
c   -- var.elim.:  2000/16002          
c   -- var.elim.:  3000/16002          
c   -- var.elim.:  4000/16002          
c   -- var.elim.:  5000/16002          
c   -- var.elim.:  6000/16002          
c   -- var.elim.:  7000/16002          
c   -- var.elim.:  8000/16002          
c   -- var.elim.:  9000/16002          
c   -- var.elim.:  10000/16002          
c   -- var.elim.:  11000/16002          
c   -- var.elim.:  12000/16002          
c   -- var.elim.:  13000/16002          
c   -- var.elim.:  14000/16002          
c   -- var.elim.:  15000/16002          
c   -- var.elim.:  16000/16002          
c   -- var.elim.:  16002/16002          
c   -- var.elim.:  1000/1847          
c   -- var.elim.:  1847/1847          
c   -- var.elim.:  194/194          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  465/465          
c   -- var.elim.:  318/318          
c   -- var.elim.:  15/15          
c   -- subsuming                       
c   -- var.elim.:  170/170          
c   -- var.elim.:  77/77          
c |     57653 |  197352   650619 |      --   56767       --      -- |     --   | -1724/-2522
c |     57653 |  197352   650619 |   78940   54566   404650     7.4 | 17.549 % |
c |     57753 |  197352   650619 |   86834   54666   405259     7.4 | 14.252 % |
c |     57903 |  197352   650619 |   95518   54816   406112     7.4 | 14.252 % |
c |     58128 |  197311   650463 |  105048   55040   407764     7.4 | 14.266 % |
c |     58466 |  197311   650463 |  115553   55378   414764     7.5 | 14.266 % |
c |     58972 |  197311   650463 |  127108   55884   423398     7.6 | 14.266 % |
c |     59731 |  197291   650381 |  139805   56639   428885     7.6 | 14.271 % |
c |     60870 |  197291   650381 |  153785   57778   450818     7.8 | 14.271 % |
c |     62580 |  197259   650269 |  169136   59485   498319     8.4 | 14.281 % |
c |     65142 |  197051   649541 |  185854   62015   522778     8.4 | 14.351 % |
c ==============================================================================
c (current CPU-time: 148.439 s)
c ==============================================================================
c [1mFound solution: 4948468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3957866   bits: 23/22
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     67744 |  197154   650041 |   59146   64617   613679     9.5 | 14.351 % |
c   -- subsuming                       
c   -- var.elim.:  376/376          
c   -- var.elim.:  199/199          
c   -- var.elim.:  36/36          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  73/73          
c   -- var.elim.:  12/12          
c |     67744 |  197015   649757 |      --   64617       --      -- |     --   | -139/-274
c |     67744 |  197015   649757 |   78806   64299   606129     9.4 | 14.351 % |
c |     67844 |  197015   649757 |   86686   64399   606889     9.4 | 14.386 % |
c |     67994 |  197015   649757 |   95355   64549   608058     9.4 | 14.386 % |
c |     68220 |  197015   649757 |  104890   64775   610018     9.4 | 14.386 % |
c |     68557 |  196968   649560 |  115352   65110   612582     9.4 | 14.403 % |
c |     69063 |  196968   649560 |  126887   65616   616964     9.4 | 14.403 % |
c |     69822 |  196968   649560 |  139576   66375   626259     9.4 | 14.403 % |
c |     70963 |  196924   649415 |  153499   67496   645366     9.6 | 14.420 % |
c |     72671 |  196911   649363 |  168838   69199   708808    10.2 | 14.422 % |
c |     75233 |  196810   648979 |  185627   71756   741837    10.3 | 14.449 % |
c |     79079 |  196810   648979 |  204189   75602   848570    11.2 | 14.449 % |
c ==============================================================================
c (current CPU-time: 181.572 s)
c ==============================================================================
c [1mFound solution: 4228653[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4677681   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     81490 |  196871   649275 |   59061   78013   914274    11.7 | 14.449 % |
c   -- subsuming                       
c   -- var.elim.:  248/248          
c   -- var.elim.:  174/174          
c   -- var.elim.:  22/22          
c   -- var.elim.:  14/14          
c   -- subsuming                       
c   -- var.elim.:  70/70          
c   -- var.elim.:  32/32          
c |     81490 |  196759   649083 |      --   78013       --      -- |     --   | -112/-183
c |     81490 |  196759   649083 |   78703   77884   910761    11.7 | 14.449 % |
c |     81590 |  196722   648931 |   86557   77982   911192    11.7 | 14.493 % |
c |     81740 |  196722   648931 |   95213   78132   911892    11.7 | 14.493 % |
c |     81965 |  196692   648834 |  104718   78356   912983    11.7 | 14.505 % |
c |     82302 |  196623   648618 |  115150   78685   914684    11.6 | 14.529 % |
c |     82808 |  196574   648444 |  126633   79190   918227    11.6 | 14.546 % |
c |     83567 |  196574   648444 |  139297   79949   923831    11.6 | 14.546 % |
c |     84706 |  196574   648444 |  153226   81088   936192    11.5 | 14.546 % |
c |     86414 |  196511   648205 |  168495   82772   951395    11.5 | 14.565 % |
c |     88977 |  196511   648205 |  185345   85335   976033    11.4 | 14.565 % |
c |     92821 |  196511   648205 |  203879   89179  1586770    17.8 | 14.565 % |
c |     98587 |  196473   648069 |  224224   94937  1846072    19.4 | 14.575 % |
c |    107236 |  196473   648069 |  246646  103586  3976741    38.4 | 14.575 % |
c ==============================================================================
c (current CPU-time: 256.913 s)
c ==============================================================================
c [1mFound solution: 3902655[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5003679   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    118206 |  196490   648199 |   58946  114551  4537297    39.6 | 14.575 % |
c   -- subsuming                       
c   -- var.elim.:  246/246          
c   -- var.elim.:  168/168          
c   -- subsuming                       
c   -- var.elim.:  48/48          
c   -- var.elim.:  7/7          
c |    118206 |  196427   648127 |      --  114551       --      -- |     --   | -63/-64
c |    118206 |  196427   648127 |   78570  113978  4204874    36.9 | 14.575 % |
c |    118306 |  196427   648127 |   86427   21534  1023646    47.5 | 14.608 % |
c |    118456 |  196427   648127 |   95070   21684  1024441    47.2 | 14.608 % |
c |    118681 |  196427   648127 |  104577   21909  1025511    46.8 | 14.608 % |
c |    119018 |  196427   648127 |  115035   22246  1027952    46.2 | 14.608 % |
c |    119524 |  196427   648127 |  126539   22752  1031050    45.3 | 14.608 % |
c |    120283 |  196427   648127 |  139192   23511  1035610    44.0 | 14.608 % |
c |    121422 |  196427   648127 |  153112   24650  1044274    42.4 | 14.608 % |
c |    123130 |  196404   648036 |  168403   26357  1056657    40.1 | 14.615 % |
c |    125692 |  196360   647875 |  185202   28917  1071821    37.1 | 14.629 % |
c |    129536 |  196329   647773 |  203690   32747  1114291    34.0 | 14.642 % |
c |    135303 |  196295   647637 |  224021   38509  1202444    31.2 | 14.651 % |
c |    143952 |  196239   647384 |  246352   47144  1329194    28.2 | 14.666 % |
c |    156926 |  196231   647352 |  270977   60117  1641980    27.3 | 14.668 % |
c |    176387 |  196202   647236 |  298030   79575  2758206    34.7 | 14.675 % |
c |    205579 |  195969   646395 |  327444  108737  4434254    40.8 | 14.750 % |
c ==============================================================================
c (current CPU-time: 440.527 s)
c ==============================================================================
c [1mFound solution: 3884670[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5021664   bits: 24/23
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    225697 |  196008   646670 |   58802  128855  5335166    41.4 | 14.750 % |
c   -- subsuming                       
c   -- var.elim.:  405/405          
c   -- var.elim.:  280/280          
c   -- var.elim.:  29/29          
c   -- var.elim.:  7/7          
c   -- subsuming                       
c   -- var.elim.:  75/75          
c   -- var.elim.:  36/36          
c   -- var.elim.:  8/8          
c |    225697 |  195833   646346 |      --  128855       --      -- |     --   | -175/-314
c |    225697 |  195833   646346 |   78333  126350  5145355    40.7 | 14.750 % |
c |    225797 |  195833   646346 |   86166   19721   577970    29.3 | 14.812 % |
c |    225947 |  195833   646346 |   94783   19871   578615    29.1 | 14.812 % |
c |    226172 |  195833   646346 |  104261   20096   579720    28.8 | 14.812 % |
c |    226509 |  195818   646278 |  114678   20432   581716    28.5 | 14.814 % |
c |    227015 |  195818   646278 |  126146   20938   584479    27.9 | 14.814 % |
c |    227774 |  195818   646278 |  138761   21697   599079    27.6 | 14.814 % |
c |    228914 |  195818   646278 |  152637   22837   604395    26.5 | 14.814 % |
c |    230622 |  195767   646103 |  167857   24538   613279    25.0 | 14.833 % |
c |    233184 |  195748   646037 |  184625   27098   630052    23.3 | 14.841 % |
c |    237029 |  195732   645979 |  203071   30942   656532    21.2 | 14.846 % |
c |    242796 |  195709   645886 |  223352   36708   719627    19.6 | 14.853 % |
c |    251445 |  195577   645412 |  245521   45344   801082    17.7 | 14.896 % |
c |    264419 |  195568   645379 |  270061   58301   984509    16.9 | 14.899 % |
c |    283881 |  195548   645317 |  297037   77762  1509701    19.4 | 14.904 % |
c |    313073 |  195411   644834 |  326512  106932  3633026    34.0 | 14.950 % |
c |    356862 |  195340   644606 |  359032  150712  6453171    42.8 | 14.976 % |
c |    422547 |  195286   644415 |  394826  216390 15252145    70.5 | 14.996 % |
c |    521073 |  195286   644415 |  434309  314916 25567941    81.2 | 14.996 % |
c ==============================================================================
c (current CPU-time: 1198.19 s)
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 X1_bit_4 X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 X2_bit_6 -X2_bit_5 X2_bit_4 X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 X4_bit_6 X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 X4_bit_1 X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 X6_bit_7 X6_bit_6 X6_bit_5 X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 X7_bit_6 X7_bit_5 X7_bit_4 X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 X8_bit_6 -X8_bit_5 -X8_bit_4 X8_bit_3 -X8_bit_2 X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 X9_bit_6 X9_bit_5 X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 X10_bit_5 -X10_bit_4 X10_bit_3 X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 -X11_bit_6 -X11_bit_5 X11_bit_4 X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 X12_bit_6 X12_bit_5 X12_bit_4 X12_bit_3 X12_bit_2 X12_bit_1 X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 X13_bit_7 X13_bit_6 X13_bit_5 X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 -X18_bit_6 X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 X19_bit_5 X19_bit_4 -X19_bit_3 -X19_bit_2 X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 -X21_bit_6 -X21_bit_5 X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 X24_bit_5 X24_bit_4 -X24_bit_3 X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 -X25_bit_5 X25_bit_4 -X25_bit_3 X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 X27_bit_6 X27_bit_5 X27_bit_4 X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 X29_bit_6 -X29_bit_5 X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 X32_bit_7 -X32_bit_6 -X32_bit_5 X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 -X34_bit_6 X34_bit_5 -X34_bit_4 -X34_bit_3 X34_bit_2 X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 X36_bit_7 -X36_bit_6 -X36_bit_5 X36_bit_4 X36_bit_3 -X36_bit_2 X36_bit_1 X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 X37_bit_1 X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 X38_bit_6 X38_bit_5 X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 X40_bit_6 X40_bit_5 X40_bit_4 X40_bit_3 -X40_bit_2 X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 X41_bit_5 -X41_bit_4 -X41_bit_3 X41_bit_2 -X41_bit_1 X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 X42_bit_7 -X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 X44_bit_6 X44_bit_5 X44_bit_4 X44_bit_3 X44_bit_2 -X44_bit_1 X44_bit0 X44_bit1 X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 X47_bit_6 -X47_bit_5 X47_bit_4 X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 X49_bit_5 X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 X51_bit_6 X51_bit_5 X51_bit_4 -X51_bit_3 X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 X52_bit_5 -X52_bit_4 -X52_bit_3 X52_bit_2 -X52_bit_1 X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 X53_bit_5 -X53_bit_4 X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 X54_bit_6 X54_bit_5 X54_bit_4 X54_bit_3 X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 X56_bit_6 X56_bit_5 -X56_bit_4 -X56_bit_3 X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 X57_bit_6 X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 X59_bit_5 X59_bit_4 X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 X60_bit_4 X60_bit_3 -X60_bit_2 X60_bit_1 X60_bit0 X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 X63_bit2 X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 -X64_bit_6 X64_bit_5 X64_bit_4 -X64_bit_3 -X64_bit_2 X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 X65_bit_3 -X65_bit_2 X65_bit_1 -X65_bit0 X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 X66_bit_1 -X66_bit0 X66_bit1 -X66_bit2 X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 X68_bit_5 X68_bit_4 X68_bit_3 -X68_bit_2 X68_bit_1 X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 X71_bit_1 -X71_bit0 X71_bit1 X71_bit2 X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 X72_bit_5 X72_bit_4 X72_bit_3 X72_bit_2 X72_bit_1 -X72_bit0 X72_bit1 X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 X73_bit_7 X73_bit_6 X73_bit_5 -X73_bit_4 -X73_bit_3 X73_bit_2 -X73_bit_1 X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 X74_bit_5 X74_bit_4 X74_bit_3 X74_bit_2 -X74_bit_1 X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 X75_bit_3 X75_bit_2 -X75_bit_1 X75_bit0 -X75_bit1 -X75_bit2 X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 -X76_bit_6 -X76_bit_5 X76_bit_4 X76_bit_3 X76_bit_2 -X76_bit_1 X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 -X77_bit_5 -X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 X78_bit_1 X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 -X79_bit_6 X79_bit_5 X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 -X82_bit_6 X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 X86_bit_7 X86_bit_6 X86_bit_5 X86_bit_4 -X86_bit_3 -X86_bit_2 X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 X89_bit_5 X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 -X92_bit_5 X92_bit_4 X92_bit_3 X92_bit_2 -X92_bit_1 X92_bit0 X92_bit1 -X92_bit2 X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 X94_bit_3 X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 X95_bit_6 -X95_bit_5 X95_bit_4 -X95_bit_3 X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 X101_bit_1 X101_bit0 X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 X103_bit_7 X103_bit_6 -X103_bit_5 -X103_bit_4 X103_bit_3 -X103_bit_2 X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 X105_bit_6 X105_bit_5 -X105_bit_4 -X105_bit_3 X105_bit_2 -X105_bit_1 X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 -X106_bit_6 X106_bit_5 X106_bit_4 X106_bit_3 X106_bit_2 X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 X107_bit_6 -X107_bit_5 X107_bit_4 X107_bit_3 X107_bit_2 X107_bit_1 X107_bit0 -X107_bit1 -X107_bit2 X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 X108_bit_2 -X108_bit_1 X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 X110_bit_1 X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 -X111_bit_5 X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 X113_bit_6 -X113_bit_5 X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 X114_bit0 X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 X115_bit_6 X115_bit_5 X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 X116_bit_6 X116_bit_5 X116_bit_4 -X116_bit_3 X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 X118_bit_6 -X118_bit_5 X118_bit_4 -X118_bit_3 X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 X120_bit_6 X120_bit_5 X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 X120_bit0 X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 X123_bit_7 X123_bit_6 -X123_bit_5 -X123_bit_4 X123_bit_3 -X123_bit_2 -X123_bit_1 X123_bit0 X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 X124_bit_5 -X124_bit_4 X124_bit_3 X124_bit_2 -X124_bit_1 X124_bit0 -X124_bit1 X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 X125_bit_6 X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 X125_bit0 X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 X132_bit_2 X132_bit_1 X132_bit0 X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 X134_bit_7 -X134_bit_6 X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 X137_bit_6 X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 X138_bit_7 X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 X140_bit1 X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 X148_bit_6 X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 X162_bit_6 X162_bit_5 -X162_bit_4 X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 X162_bit2 -X162_bit3 X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 X164_bit_6 X164_bit_5 -X164_bit_4 X164_bit_3 X164_bit_2 -X164_bit_1 X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 X165_bit_6 X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 X166_bit_6 X166_bit_5 X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 X169_bit_7 X169_bit_6 X169_bit_5 -X169_bit_4 X169_bit_3 X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 X171_bit_6 X171_bit_5 -X171_bit_4 -X171_bit_3 X171_bit_2 X171_bit_1 X171_bit0 -X171_bit1 X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 X172_bit_6 X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 X172_bit_1 X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 X173_bit_6 X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 -X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 X179_bit_6 X179_bit_5 X179_bit_4 -X179_bit_3 -X179_bit_2 X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 X180_bit_6 X180_bit_5 -X180_bit_4 X180_bit_3 X180_bit_2 X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 X181_bit_5 X181_bit_4 -X181_bit_3 -X181_bit_2 X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 X182_bit_7 X182_bit_6 X182_bit_5 X182_bit_4 X182_bit_3 X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 -X184_bit_6 X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 X186_bit_1 X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 X192_bit_6 -X192_bit_5 X192_bit_4 X192_bit_3 -X192_bit_2 -X192_bit_1 X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 X193_bit_6 X193_bit_5 -X193_bit_4 X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 X196_bit_6 -X196_bit_5 X196_bit_4 X196_bit_3 X196_bit_2 X196_bit_1 X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 -X197_bit_5 X197_bit_4 X197_bit_3 X197_bit_2 X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 X198_bit_5 X198_bit_4 -X198_bit_3 -X198_bit_2 X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 -X200_bit_6 -X200_bit_5 X200_bit_4 -X200_bit_3 -X200_bit_2 X200_bit_1 -X200_bit0 -X200_bit1 X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 X201_bit_7 X201_bit_6 X201_bit_5 -X201_bit_4 X201_bit_3 -X201_bit_2 -X201_bit_1 X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 X203_bit_6 X203_bit_5 X203_bit_4 X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 X204_bit_6 -X204_bit_5 X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 X205_bit_5 X205_bit_4 X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 X207_bit_6 X207_bit_5 X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 -X208_bit_5 X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 X209_bit_6 X209_bit_5 X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 X210_bit1 -X210_bit2 X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 X211_bit_7 X211_bit_6 X211_bit_5 X211_bit_4 -X211_bit_3 X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 X212_bit_3 X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 X213_bit_7 -X213_bit_6 X213_bit_5 -X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 X214_bit_6 X214_bit_5 X214_bit_4 X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 X216_bit_6 X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 X219_bit_5 X219_bit_4 X219_bit_3 -X219_bit_2 X219_bit_1 X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 X220_bit_7 X220_bit_6 -X220_bit_5 X220_bit_4 X220_bit_3 X220_bit_2 -X220_bit_1 X220_bit0 -X220_bit1 X220_bit2 X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 -X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 X224_bit_7 X224_bit_6 X224_bit_5 X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 X226_bit_7 X226_bit_6 -X226_bit_5 X226_bit_4 -X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 X226_bit2 X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 -X227_bit_4 -X227_bit_3 X227_bit_2 X227_bit_1 -X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 -X228_bit_5 -X228_bit_4 X228_bit_3 X228_bit_2 X228_bit_1 X228_bit0 -X228_bit1 X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 -X230_bit_6 -X230_bit_5 -X230_bit_4 -X230_bit_3 -X230_bit_2 -X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 X232_bit_6 -X232_bit_5 X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 X233_bit_6 X233_bit_5 -X233_bit_4 -X233_bit_3 X233_bit_2 -X233_bit_1 X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 -X234_bit_5 -X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 X235_bit_6 X235_bit_5 -X235_bit_4 X235_bit_3 X235_bit_2 -X235_bit_1 X235_bit0 -X235_bit1 -X235_bit2 X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 X236_bit_6 -X236_bit_5 X236_bit_4 X236_bit_3 -X236_bit_2 -X236_bit_1 X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 -X237_bit_6 -X237_bit_5 X237_bit_4 -X237_bit_3 -X237_bit_2 X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 X239_bit_6 X239_bit_5 X239_bit_4 X239_bit_3 X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 X240_bit_6 -X240_bit_5 -X240_bit_4 X240_bit_3 X240_bit_2 X240_bit_1 X240_bit0 -X240_bit1 X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 X241_bit_6 -X241_bit_5 X241_bit_4 X241_bit_3 -X241_bit_2 X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 X242_bit_3 X242_bit_2 -X242_bit_1 -X242_bit0 X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 X243_bit_4 X243_bit_3 X243_bit_2 X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 X246_bit_6 -X246_bit_5 X246_bit_4 X246_bit_3 -X246_bit_2 X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 -X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 X247_bit2 X247_bit3 X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 -X250_bit_3 -X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 X251_bit_6 -X251_bit_5 X251_bit_4 -X251_bit_3 X251_bit_2 -X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 -X252_bit_6 -X252_bit_5 -X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 X253_bit_6 -X253_bit_5 X253_bit_4 -X253_bit_3 X253_bit_2 X253_bit_1 -X253_bit0 -X253_bit1 X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 -X254_bit_6 -X254_bit_5 -X254_bit_4 X254_bit_3 -X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 X255_bit_6 -X255_bit_5 -X255_bit_4 X255_bit_3 -X255_bit_2 X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -Y0_bit0 Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 Y11_bit0 Y12_bit0 Y13_bit0 Y14_bit0 -Y15_bit0 -Y16_bit0 -Y17_bit0 Y18_bit0 Y19_bit0 -Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 Y25_bit0 Y26_bit0 Y27_bit0 -Y28_bit0 Y29_bit0 Y30_bit0 -Y31_bit0 Y32_bit0 -Y33_bit0 Y34_bit0 -Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 -Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 -Y50_bit0 Y51_bit0 Y52_bit0 Y53_bit0 Y54_bit0 -Y55_bit0 Y56_bit0 Y57_bit0 -Y58_bit0 Y59_bit0 Y60_bit0 -Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 Y66_bit0 -Y67_bit0 Y68_bit0 -Y69_bit0 -Y70_bit0 Y71_bit0 Y72_bit0 Y73_bit0 Y74_bit0 Y75_bit0 Y76_bit0 -Y77_bit0 Y78_bit0 Y79_bit0 -Y80_bit0 -Y81_bit0 Y82_bit0 -Y83_bit0 -Y84_bit0 -Y85_bit0 Y86_bit0 Y87_bit0 Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 Y95_bit0 -Y96_bit0 -Y97_bit0 -Y98_bit0 -Y99_bit0 -Y100_bit0 Y101_bit0 -Y102_bit0 Y103_bit0 -Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 -Y109_bit0 Y110_bit0 Y111_bit0 -Y112_bit0 Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 -Y117_bit0 Y118_bit0 Y119_bit0 Y120_bit0 -Y121_bit0 -Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 -Y128_bit0 -Y129_bit0 -Y130_bit0 Y131_bit0 Y132_bit0 Y133_bit0 Y134_bit0 -Y135_bit0 Y136_bit0 Y137_bit0 Y138_bit0 -Y139_bit0 Y140_bit0 Y141_bit0 Y142_bit0 Y143_bit0 -Y144_bit0 -Y145_bit0 Y146_bit0 -Y147_bit0 Y148_bit0 Y149_bit0 Y150_bit0 -Y151_bit0 -Y152_bit0 Y153_bit0 Y154_bit0 -Y155_bit0 -Y156_bit0 -Y157_bit0 -Y158_bit0 -Y159_bit0 -Y160_bit0 -Y161_bit0 Y162_bit0 Y163_bit0 Y164_bit0 Y165_bit0 Y166_bit0 -Y167_bit0 -Y168_bit0 Y169_bit0 -Y170_bit0 Y171_bit0 Y172_bit0 Y173_bit0 -Y174_bit0 Y175_bit0 Y176_bit0 -Y177_bit0 -Y178_bit0 Y179_bit0 Y180_bit0 Y181_bit0 Y182_bit0 -Y183_bit0 Y184_bit0 -Y185_bit0 Y186_bit0 -Y187_bit0 -Y188_bit0 -Y189_bit0 -Y190_bit0 -Y191_bi#### 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.89 0.94 0.90 2/54 30267
Raw data (stat): 30267 (runsolver) R 30266 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482811328 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99967 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8360 0 0 0 959 27 0 0 25 0 1 0 482811328 34942976 7242 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8531 7242 603 41 0 8490 0
vsize: 34124
[startup+20.0005 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8376 0 0 0 1960 27 0 0 25 0 1 0 482811328 34942976 7258 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8531 7258 603 41 0 8490 0
vsize: 34124
[startup+30.0029 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8382 0 0 0 2960 27 0 0 25 0 1 0 482811328 35139584 7264 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 7264 603 41 0 8538 0
vsize: 34316
[startup+40.0062 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8387 0 0 0 3960 27 0 0 25 0 1 0 482811328 35139584 7269 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 7269 603 41 0 8538 0
vsize: 34316
[startup+50.0064 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8413 0 0 0 4960 27 0 0 25 0 1 0 482811328 35139584 7295 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 7295 603 41 0 8538 0
vsize: 34316
[startup+60.0062 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8482 0 0 0 5960 27 0 0 25 0 1 0 482811328 35536896 7364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8676 7364 603 41 0 8635 0
vsize: 34704
[startup+70.0068 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8596 0 0 0 6960 28 0 0 25 0 1 0 482811328 36069376 7478 4294967295 134512640 134672761 3221224544 3221223692 134566158 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8806 7478 603 41 0 8765 0
vsize: 35224
[startup+80.007 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8667 0 0 0 7960 28 0 0 25 0 1 0 482811328 36335616 7549 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8871 7549 603 41 0 8830 0
vsize: 35484
[startup+90.0079 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8780 0 0 0 8959 29 0 0 25 0 1 0 482811328 36732928 7662 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8968 7662 603 41 0 8927 0
vsize: 35872
[startup+100.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8821 0 0 0 9959 29 0 0 25 0 1 0 482811328 36868096 7703 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9001 7703 603 41 0 8960 0
vsize: 36004
[startup+110.008 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8877 0 0 0 10959 30 0 0 25 0 1 0 482811328 37138432 7759 4294967295 134512640 134672761 3221224544 3221223496 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9067 7759 603 41 0 9026 0
vsize: 36268
[startup+120.009 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 8953 0 0 0 11959 30 0 0 25 0 1 0 482811328 37408768 7835 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9133 7835 603 41 0 9092 0
vsize: 36532
[startup+130.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 18843 0 0 0 12932 56 0 0 25 0 1 0 482811328 61710336 13710 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15066 13710 603 41 0 15025 0
vsize: 60264
[startup+140.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 18948 0 0 0 13932 56 0 0 25 0 1 0 482811328 62246912 13815 4294967295 134512640 134672761 3221224544 3221223728 134615848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15197 13815 603 41 0 15156 0
vsize: 60788
[startup+150.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 21100 0 0 0 14927 61 0 0 25 0 1 0 482811328 63270912 14078 4294967295 134512640 134672761 3221224544 3221221968 134522889 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15447 14078 603 41 0 15406 0
vsize: 61788
[startup+160.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 22013 0 0 0 15924 64 0 0 25 0 1 0 482811328 63934464 14211 4294967295 134512640 134672761 3221224544 3221223688 134616111 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15609 14211 603 41 0 15568 0
vsize: 62436
[startup+170.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 22079 0 0 0 16924 64 0 0 25 0 1 0 482811328 64200704 14277 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15674 14277 603 41 0 15633 0
vsize: 62696
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 22303 0 0 0 17923 65 0 0 25 0 1 0 482811328 65003520 14501 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15870 14501 603 41 0 15829 0
vsize: 63480
[startup+190.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 24974 0 0 0 18915 71 0 0 25 0 1 0 482811328 65736704 14685 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 14685 603 41 0 16008 0
vsize: 64196
[startup+200.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 24978 0 0 0 19916 71 0 0 25 0 1 0 482811328 65736704 14689 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16049 14689 603 41 0 16008 0
vsize: 64196
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 25132 0 0 0 20916 72 0 0 25 0 1 0 482811328 66404352 14843 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16212 14843 603 41 0 16171 0
vsize: 64848
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 25900 0 0 0 21914 74 0 0 25 0 1 0 482811328 69562368 15611 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16983 15611 603 41 0 16942 0
vsize: 67932
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 27026 0 0 0 22912 76 0 0 25 0 1 0 482811328 74174464 16737 4294967295 134512640 134672761 3221224544 3221223584 134613768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18109 16738 603 41 0 18068 0
vsize: 72436
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 28223 0 0 0 23909 79 0 0 25 0 1 0 482811328 78946304 17934 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19274 17934 603 41 0 19233 0
vsize: 77096
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 28503 0 0 0 24909 79 0 0 25 0 1 0 482811328 80150528 18214 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19568 18214 603 41 0 19527 0
vsize: 78272
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31511 0 0 0 25901 87 0 0 25 0 1 0 482811328 82276352 18755 4294967295 134512640 134672761 3221224544 3221223920 134620815 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20087 18755 603 41 0 20046 0
vsize: 80348
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 26901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 27901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 28901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 29901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 30901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 31901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223668 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 32901 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 33902 87 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 34901 88 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 35901 88 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 36901 88 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 37901 88 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223584 134603510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31714 0 0 0 38901 88 0 0 25 0 1 0 482811328 82800640 18846 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 18846 603 41 0 20174 0
vsize: 80860
[startup+400.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31722 0 0 0 39902 88 0 0 25 0 1 0 482811328 82931712 18854 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20247 18854 603 41 0 20206 0
vsize: 80988
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 31909 0 0 0 40901 88 0 0 25 0 1 0 482811328 83603456 19041 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20411 19041 603 41 0 20370 0
vsize: 81644
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 32164 0 0 0 41901 89 0 0 25 0 1 0 482811328 84672512 19296 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20672 19296 603 41 0 20631 0
vsize: 82688
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 32436 0 0 0 42900 90 0 0 25 0 1 0 482811328 85737472 19568 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20932 19568 603 41 0 20891 0
vsize: 83728
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 32822 0 0 0 43899 91 0 0 25 0 1 0 482811328 87339008 19954 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21323 19954 603 41 0 21282 0
vsize: 85292
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 44890 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 45890 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 46890 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 47890 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+490.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 48890 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 49891 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 50891 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 51891 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 52891 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 53891 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 54892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 55892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 56892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223584 134612966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 57892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 58892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 59892 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 35789 0 0 0 60893 100 0 0 25 0 1 0 482811328 88436736 20250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21591 20250 603 41 0 21550 0
vsize: 86364
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 36278 0 0 0 61891 101 0 0 25 0 1 0 482811328 90423296 20739 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22076 20739 603 41 0 22035 0
vsize: 88304
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 36663 0 0 0 62890 103 0 0 25 0 1 0 482811328 92540928 21124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22593 21124 603 41 0 22552 0
vsize: 90372
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 36880 0 0 0 63890 103 0 0 25 0 1 0 482811328 93515776 21341 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22831 21341 603 41 0 22790 0
vsize: 91324
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 37113 0 0 0 64889 104 0 0 25 0 1 0 482811328 94449664 21574 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23059 21574 603 41 0 23018 0
vsize: 92236
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 37359 0 0 0 65889 105 0 0 25 0 1 0 482811328 95379456 21820 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23286 21820 603 41 0 23245 0
vsize: 93144
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 37802 0 0 0 66887 106 0 0 25 0 1 0 482811328 97091584 22263 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23704 22263 603 41 0 23663 0
vsize: 94816
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 39005 0 0 0 67884 110 0 0 25 0 1 0 482811328 101994496 23466 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24934 23466 603 41 0 24893 0
vsize: 99604
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 40218 0 0 0 68881 113 0 0 25 0 1 0 482811328 107048960 24679 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26135 24679 603 41 0 26094 0
vsize: 104540
[startup+700.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 41119 0 0 0 69879 115 0 0 25 0 1 0 482811328 110628864 25580 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27009 25580 603 41 0 26968 0
vsize: 108036
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 42024 0 0 0 70876 118 0 0 25 0 1 0 482811328 114339840 26485 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27915 26485 603 41 0 27874 0
vsize: 111660
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 43144 0 0 0 71874 120 0 0 25 0 1 0 482811328 118960128 27605 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29043 27605 603 41 0 29002 0
vsize: 116172
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 44018 0 0 0 72873 122 0 0 25 0 1 0 482811328 122572800 28479 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29925 28479 603 41 0 29884 0
vsize: 119700
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 44100 0 0 0 73872 123 0 0 25 0 1 0 482811328 122839040 28561 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29990 28561 603 41 0 29949 0
vsize: 119960
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 44299 0 0 0 74872 123 0 0 25 0 1 0 482811328 123633664 28760 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30184 28760 603 41 0 30143 0
vsize: 120736
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 44986 0 0 0 75870 125 0 0 25 0 1 0 482811328 126402560 29447 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30860 29447 603 41 0 30819 0
vsize: 123440
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 45842 0 0 0 76868 127 0 0 25 0 1 0 482811328 129839104 30303 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31699 30303 603 41 0 31658 0
vsize: 126796
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 46349 0 0 0 77867 129 0 0 25 0 1 0 482811328 131964928 30810 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32218 30810 603 41 0 32177 0
vsize: 128872
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 46862 0 0 0 78866 129 0 0 25 0 1 0 482811328 134098944 31323 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32739 31323 603 41 0 32698 0
vsize: 130956
[startup+800.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 47277 0 0 0 79865 131 0 0 25 0 1 0 482811328 135692288 31738 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33128 31738 603 41 0 33087 0
vsize: 132512
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 47496 0 0 0 80865 131 0 0 25 0 1 0 482811328 136630272 31957 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33357 31957 603 41 0 33316 0
vsize: 133428
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 47894 0 0 0 81864 132 0 0 25 0 1 0 482811328 138248192 32355 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33752 32355 603 41 0 33711 0
vsize: 135008
[startup+830.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 48239 0 0 0 82862 134 0 0 25 0 1 0 482811328 139571200 32700 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34075 32700 603 41 0 34034 0
vsize: 136300
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 48677 0 0 0 83861 136 0 0 25 0 1 0 482811328 141426688 33138 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34528 33138 603 41 0 34487 0
vsize: 138112
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 49088 0 0 0 84860 137 0 0 25 0 1 0 482811328 143138816 33549 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34946 33549 603 41 0 34905 0
vsize: 139784
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 49476 0 0 0 85858 139 0 0 25 0 1 0 482811328 144732160 33937 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35335 33937 603 41 0 35294 0
vsize: 141340
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 49832 0 0 0 86857 140 0 0 25 0 1 0 482811328 146042880 34293 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35655 34293 603 41 0 35614 0
vsize: 142620
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 50192 0 0 0 87856 142 0 0 25 0 1 0 482811328 147632128 34653 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36043 34653 603 41 0 36002 0
vsize: 144172
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 50536 0 0 0 88855 143 0 0 25 0 1 0 482811328 149082112 34997 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36397 34997 603 41 0 36356 0
vsize: 145588
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 50884 0 0 0 89854 144 0 0 25 0 1 0 482811328 150401024 35345 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36719 35345 603 41 0 36678 0
vsize: 146876
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 51264 0 0 0 90853 145 0 0 25 0 1 0 482811328 153083904 35725 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37374 35725 603 41 0 37333 0
vsize: 149496
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 51637 0 0 0 91853 146 0 0 25 0 1 0 482811328 154537984 36098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37729 36098 603 41 0 37688 0
vsize: 150916
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 51996 0 0 0 92852 146 0 0 25 0 1 0 482811328 156049408 36457 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38098 36457 603 41 0 38057 0
vsize: 152392
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 52315 0 0 0 93851 147 0 0 25 0 1 0 482811328 157474816 36776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38446 36776 603 41 0 38405 0
vsize: 153784
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 52613 0 0 0 94850 148 0 0 25 0 1 0 482811328 158769152 37074 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38762 37074 603 41 0 38721 0
vsize: 155048
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 52907 0 0 0 95850 149 0 0 25 0 1 0 482811328 159870976 37368 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39031 37368 603 41 0 38990 0
vsize: 156124
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 53204 0 0 0 96849 150 0 0 25 0 1 0 482811328 161087488 37665 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39328 37665 603 41 0 39287 0
vsize: 157312
[startup+980.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 53487 0 0 0 97849 151 0 0 25 0 1 0 482811328 162287616 37948 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39621 37948 603 41 0 39580 0
vsize: 158484
[startup+990.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 53781 0 0 0 98848 151 0 0 25 0 1 0 482811328 163483648 38242 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39913 38242 603 41 0 39872 0
vsize: 159652
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 54077 0 0 0 99847 153 0 0 25 0 1 0 482811328 164667392 38538 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40202 38538 603 41 0 40161 0
vsize: 160808
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 54354 0 0 0 100846 153 0 0 25 0 1 0 482811328 165855232 38815 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40492 38815 603 41 0 40451 0
vsize: 161968
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 54643 0 0 0 101846 154 0 0 25 0 1 0 482811328 167047168 39104 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40783 39104 603 41 0 40742 0
vsize: 163132
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 54918 0 0 0 102845 155 0 0 25 0 1 0 482811328 168116224 39379 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41044 39379 603 41 0 41003 0
vsize: 164176
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 55176 0 0 0 103845 156 0 0 25 0 1 0 482811328 169185280 39637 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41305 39637 603 41 0 41264 0
vsize: 165220
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 55408 0 0 0 104844 157 0 0 25 0 1 0 482811328 170106880 39869 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41530 39869 603 41 0 41489 0
vsize: 166120
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 55629 0 0 0 105843 158 0 0 25 0 1 0 482811328 171048960 40090 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41760 40090 603 41 0 41719 0
vsize: 167040
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 55841 0 0 0 106843 158 0 0 25 0 1 0 482811328 171835392 40302 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41952 40302 603 41 0 41911 0
vsize: 167808
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 56056 0 0 0 107842 159 0 0 25 0 1 0 482811328 172806144 40517 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42189 40517 603 41 0 42148 0
vsize: 168756
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 56270 0 0 0 108842 159 0 0 25 0 1 0 482811328 173731840 40731 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42415 40731 603 41 0 42374 0
vsize: 169660
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 56458 0 0 0 109842 160 0 0 25 0 1 0 482811328 174395392 40919 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42577 40919 603 41 0 42536 0
vsize: 170308
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 56669 0 0 0 110841 160 0 0 25 0 1 0 482811328 175337472 41130 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42807 41130 603 41 0 42766 0
vsize: 171228
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 56869 0 0 0 111841 161 0 0 25 0 1 0 482811328 176156672 41330 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43007 41330 603 41 0 42966 0
vsize: 172028
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 57076 0 0 0 112840 162 0 0 25 0 1 0 482811328 176951296 41537 4294967295 134512640 134672761 3221224544 3221223584 134603502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43201 41537 603 41 0 43160 0
vsize: 172804
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 57274 0 0 0 113839 163 0 0 25 0 1 0 482811328 177737728 41735 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43393 41735 603 41 0 43352 0
vsize: 173572
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 57497 0 0 0 114839 163 0 0 25 0 1 0 482811328 178798592 41958 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43652 41958 603 41 0 43611 0
vsize: 174608
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 57710 0 0 0 115839 164 0 0 25 0 1 0 482811328 179585024 42171 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43844 42171 603 41 0 43803 0
vsize: 175376
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 57916 0 0 0 116839 164 0 0 25 0 1 0 482811328 180506624 42377 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44069 42377 603 41 0 44028 0
vsize: 176276
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 58116 0 0 0 117838 165 0 0 25 0 1 0 482811328 181297152 42577 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44262 42577 603 41 0 44221 0
vsize: 177048
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 58310 0 0 0 118838 165 0 0 25 0 1 0 482811328 182104064 42771 4294967295 134512640 134672761 3221224544 3221223688 134616256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44459 42771 603 41 0 44418 0
vsize: 177836
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30267
Raw data (stat): 30267 (minisat+) R 30266 5897 5896 0 -1 0 60199 0 0 0 119834 169 0 0 25 0 1 0 482811328 190734336 44651 4294967295 134512640 134672761 3221224544 3221222800 134565525 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46566 44651 603 41 0 46525 0
vsize: 186264
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30267
Raw data (stat): 30267 (minisat+) Z 30266 5897 5896 0 -1 12 60200 0 0 0 119835 178 0 0 25 0 1 0 482811328 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.14
CPU user time (s): 1198.36
CPU system time (s): 1.78373
CPU usage (%): 100
Max. virtual memory (Kb): 186264
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####