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/MIPLIB/miplib2003/normalized-mps-v2-13-7-rout.opb
MD5SUM	46c175563919d1fe493ed3da6f49d52f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1251872
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	33812000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	166074535
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1585.77
Number of variables	5151
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	617
Trace number 18463

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        788180 kB
Buffers:         16764 kB
Cached:         201920 kB
SwapCached:          4 kB
Active:         138108 kB
Inactive:        83412 kB
HighTotal:      131008 kB
HighFree:        14672 kB
LowTotal:       903652 kB
LowFree:        773508 kB
SwapTotal:     2097892 kB
SwapFree:      2097820 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6804 kB
Slab:            19324 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:25:36 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 17989 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3854   maxlim: 97129415   bits: 27/27
c ---[ 319]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 318]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 317]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 316]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 315]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 314]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 313]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 312]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 311]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 310]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 309]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 308]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 307]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 306]---> Adder-cost: 16   maxlim: 4094   bits: 13/12
c ---[ 305]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 304]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 303]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 302]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 301]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 300]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 299]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 298]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 297]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 296]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 295]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 294]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 293]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 292]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 291]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 290]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 289]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 288]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 287]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 286]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 285]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 284]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 283]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 282]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 281]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 280]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 279]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 278]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 277]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 276]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 275]---> Adder-cost: 26   maxlim: 18   bits: 5/5
c ---[ 274]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 273]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 272]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 271]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 270]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 269]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 268]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 267]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 266]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 265]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 264]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 263]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 262]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 261]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 260]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 259]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 258]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 257]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 256]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 255]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 254]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 253]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 252]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 251]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 249]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 247]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 246]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 245]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 244]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 243]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 242]---> Adder-cost: 30   maxlim: 18   bits: 5/5
c ---[ 241]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 240]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 238]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 237]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 236]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 234]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 232]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 231]---> Adder-cost: 26   maxlim: 18   bits: 5/5
c ---[ 230]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 229]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 224]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 222]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 220]---> Adder-cost: 26   maxlim: 18   bits: 5/5
c ---[ 219]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 217]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 216]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 214]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 211]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 210]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 209]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 208]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 207]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 206]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 205]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 204]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 203]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 202]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 201]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 199]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 196]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 195]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 194]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 193]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 192]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 191]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 190]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 189]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 188]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 187]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 185]---> Adder-cost: 48   maxlim: 11   bits: 5/4
c ---[ 184]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 183]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 182]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 181]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 180]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 179]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 178]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 176]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 175]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 173]---> Adder-cost: 48   maxlim: 11   bits: 5/4
c ---[ 172]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 171]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 170]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 168]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 166]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 165]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 164]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 163]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 48   maxlim: 11   bits: 5/4
c ---[ 160]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 159]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 158]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 156]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 155]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 153]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 151]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 48   maxlim: 11   bits: 5/4
c ---[ 148]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 147]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 146]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 143]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 137]---> Adder-cost: 48   maxlim: 11   bits: 5/4
c ---[ 136]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 135]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 132]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 129]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 127]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 42   maxlim: 15   bits: 5/4
c ---[ 124]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 123]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 122]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 121]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 119]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 118]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 117]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 116]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 115]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 113]---> Adder-cost: 42   maxlim: 15   bits: 5/4
c ---[ 112]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 111]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 110]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 107]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 106]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 105]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 101]---> Adder-cost: 42   maxlim: 15   bits: 5/4
c ---[ 100]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  98]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  96]---> Adder-cost: 42   maxlim: 15   bits: 5/4
c ---[  94]---> Adder-cost: 42   maxlim: 15   bits: 5/4
c ---[  92]---> Adder-cost: 59   maxlim: 11   bits: 5/4
c ---[  90]---> Adder-cost: 59   maxlim: 11   bits: 5/4
c ---[  88]---> Adder-cost: 59   maxlim: 11   bits: 5/4
c ---[  86]---> Adder-cost: 59   maxlim: 11   bits: 5/4
c ---[  84]---> Adder-cost: 59   maxlim: 11   bits: 5/4
c ---[  82]---> Adder-cost: 546   maxlim: 21489   bits: 16/15
c ---[  80]---> Adder-cost: 546   maxlim: 21489   bits: 16/15
c ---[  78]---> Adder-cost: 546   maxlim: 21489   bits: 16/15
c ---[  77]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  75]---> Adder-cost: 546   maxlim: 21489   bits: 16/15
c ---[  73]---> Adder-cost: 546   maxlim: 21489   bits: 16/15
c ---[  71]---> Adder-cost: 456   maxlim: 9207   bits: 15/14
c ---[  69]---> Adder-cost: 456   maxlim: 9207   bits: 15/14
c ---[  67]---> Adder-cost: 456   maxlim: 9207   bits: 15/14
c ---[  65]---> Adder-cost: 456   maxlim: 9207   bits: 15/14
c ---[  63]---> Adder-cost: 456   maxlim: 9207   bits: 15/14
c ---[  61]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  59]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  57]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  56]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  54]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  52]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  51]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  49]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  47]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  45]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  42]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  38]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  35]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 26   maxlim: 18   bits: 5/5
c ---[  31]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  30]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  29]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  24]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  22]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  21]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[  20]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  16]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  11]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 52   maxlim: 47   bits: 6/6
c ---[   9]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   6]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   5]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   2]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   1]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   0]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  120786   438926 |   40262       0        0     nan |  0.000 % |
c |       100 |  120736   438746 |   44288      94      265     2.8 | 21.891 % |
c |       250 |  120635   438393 |   48717     236      827     3.5 | 21.938 % |
c |       475 |  120568   438170 |   53588     452     1874     4.1 | 21.985 % |
c |       813 |  120568   438170 |   58947     790    11895    15.1 | 21.985 % |
c |      1322 |  120560   438144 |   64842    1298    29904    23.0 | 21.989 % |
c |      2081 |  120560   438144 |   71326    2057    62400    30.3 | 21.989 % |
c |      3221 |  120505   437963 |   78459    3182   113459    35.7 | 22.028 % |
c |      4930 |  120473   437862 |   86305    4888   142163    29.1 | 22.051 % |
c |      7493 |  120448   437779 |   94935    7442   204162    27.4 | 22.063 % |
c |     11338 |  120408   437649 |  104429   11282   293913    26.1 | 22.082 % |
c |     17104 |  120383   437572 |  114872   17046   437879    25.7 | 22.102 % |
c |     25754 |  120375   437546 |  126359   25695   693791    27.0 | 22.105 % |
c |     38732 |  120194   436927 |  138995   38654  1084281    28.1 | 22.183 % |
c |     58195 |  119958   436130 |  152894   58091  1593003    27.4 | 22.316 % |
c |     87387 |  119622   435018 |  168184   87242  2459997    28.2 | 22.499 % |
c |    131177 |  119297   433918 |  185002  130963  3981542    30.4 | 22.662 % |
c |    196863 |  118182   430115 |  203503   24438  1041784    42.6 | 23.250 % |
c |    295390 |  116775   425248 |  223853  122750  4907596    40.0 | 23.869 % |
c ==============================================================================
c [1mFound solution: 1282112[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 28   maxlim: 25469   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    321734 |  116043   422768 |   38681  148978  7032533    47.2 | 23.869 % |
c |    321836 |  116043   422768 |   42549   25736  1092268    42.4 | 24.234 % |
c |    321987 |  116043   422768 |   46804   25887  1097849    42.4 | 24.234 % |
c |    322212 |  116043   422768 |   51484   26112  1105451    42.3 | 24.234 % |
c |    322550 |  116043   422768 |   56632   26450  1114928    42.2 | 24.234 % |
c |    323058 |  116043   422768 |   62296   26958  1127953    41.8 | 24.234 % |
c |    323817 |  116043   422768 |   68525   27717  1165522    42.1 | 24.234 % |
c ==============================================================================
c [1mFound solution: 1277472[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 30   maxlim: 25614   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    324758 |  116176   423252 |   38725   28658  1232339    43.0 | 24.234 % |
c |    324858 |  116167   423221 |   42597   28756  1235198    43.0 | 24.230 % |
c |    325010 |  116136   423116 |   46857   28901  1241679    43.0 | 24.250 % |
c |    325235 |  116136   423116 |   51542   29126  1251774    43.0 | 24.250 % |
c |    325572 |  116136   423116 |   56697   29463  1269863    43.1 | 24.250 % |
c |    326078 |  116127   423085 |   62366   29967  1275618    42.6 | 24.254 % |
c |    326837 |  116067   422873 |   68603   30722  1354350    44.1 | 24.269 % |
c |    327976 |  116067   422873 |   75464   31861  1390821    43.7 | 24.269 % |
c ==============================================================================
c [1mFound solution: 1273248[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 26   maxlim: 25746   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    329163 |  116181   423288 |   38727   33048  1513787    45.8 | 24.269 % |
c |    329264 |  116181   423288 |   42599   33149  1515029    45.7 | 24.265 % |
c |    329416 |  116181   423288 |   46859   33301  1532845    46.0 | 24.265 % |
c |    329642 |  116181   423288 |   51545   33527  1541105    46.0 | 24.265 % |
c |    329980 |  116181   423288 |   56700   33865  1557676    46.0 | 24.265 % |
c |    330486 |  116181   423288 |   62370   34371  1575273    45.8 | 24.265 % |
c |    331245 |  116181   423288 |   68607   35130  1649993    47.0 | 24.265 % |
c |    332384 |  116158   423209 |   75467   36260  1674502    46.2 | 24.281 % |
c |    334094 |  116150   423183 |   83014   37969  1761029    46.4 | 24.285 % |
c |    336657 |  115772   421871 |   91316   40496  1922879    47.5 | 24.444 % |
c |    340502 |  115746   421781 |  100447   44332  2187380    49.3 | 24.459 % |
c |    346270 |  115617   421328 |  110492   50085  2566458    51.2 | 24.513 % |
c |    354919 |  115435   420694 |  121541   58701  3219386    54.8 | 24.599 % |
c |    367894 |  115261   420090 |  133696   71643  4356770    60.8 | 24.672 % |
c ==============================================================================
c [1mFound solution: 1271456[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 25802   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    381930 |  115301   420269 |   38433   85666  4919696    57.4 | 24.672 % |
c |    382032 |  115256   420114 |   42276   24816   620756    25.0 | 24.726 % |
c |    382182 |  115256   420114 |   46503   24966   628602    25.2 | 24.726 % |
c |    382408 |  115256   420114 |   51154   25192   700184    27.8 | 24.726 % |
c |    382745 |  114961   419101 |   56269   25496   711032    27.9 | 24.885 % |
c |    383251 |  114961   419101 |   61896   26002   717630    27.6 | 24.885 % |
c |    384010 |  114961   419101 |   68086   26761   750530    28.0 | 24.885 % |
c |    385151 |  114961   419101 |   74895   27902   775635    27.8 | 24.885 % |
c |    386859 |  114961   419101 |   82384   29610   854230    28.8 | 24.885 % |
c ==============================================================================
c [1mFound solution: 1265376[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 28   maxlim: 25992   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    389289 |  115089   419560 |   38363   32040  1068851    33.4 | 24.885 % |
c |    389389 |  115089   419560 |   42199   32140  1071771    33.3 | 24.878 % |
c |    389541 |  115089   419560 |   46419   32292  1079007    33.4 | 24.878 % |
c |    389768 |  115089   419560 |   51061   32519  1090798    33.5 | 24.878 % |
c |    390106 |  115089   419560 |   56167   32857  1103792    33.6 | 24.878 % |
c |    390613 |  115089   419560 |   61783   33364  1161073    34.8 | 24.878 % |
c |    391372 |  115089   419560 |   67962   34123  1196395    35.1 | 24.878 % |
c |    392511 |  115089   419560 |   74758   35262  1247782    35.4 | 24.878 % |
c |    394219 |  115089   419560 |   82234   36970  1315117    35.6 | 24.878 % |
c |    396782 |  115057   419450 |   90457   39522  1448004    36.6 | 24.898 % |
c |    400626 |  114949   419082 |   99503   43349  1695639    39.1 | 24.959 % |
c |    406393 |  114807   418592 |  109454   49094  2123612    43.3 | 25.044 % |
c |    415042 |  114417   417240 |  120399   57699  3059425    53.0 | 25.257 % |
c |    428017 |  114100   416139 |  132439   70628  3563914    50.5 | 25.412 % |
c |    447479 |  113929   415544 |  145683   90064  5529870    61.4 | 25.497 % |
c ==============================================================================
c [1mFound solution: 1261888[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 24   maxlim: 26101   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    451614 |  114068   416087 |   38022   94199  6379551    67.7 | 25.497 % |
c |    451717 |  114034   415969 |   41824   25771  1835858    71.2 | 25.525 % |
c |    451868 |  114017   415910 |   46006   25921  1840886    71.0 | 25.537 % |
c |    452093 |  114017   415910 |   50607   26146  1855823    71.0 | 25.537 % |
c |    452431 |  114017   415910 |   55668   26484  1860346    70.2 | 25.537 % |
c |    452937 |  114017   415910 |   61234   26990  1897182    70.3 | 25.537 % |
c |    453696 |  114017   415910 |   67358   27749  1917808    69.1 | 25.537 % |
c |    454838 |  114017   415910 |   74094   28891  1999424    69.2 | 25.537 % |
c |    456546 |  114000   415859 |   81503   30598  2174548    71.1 | 25.552 % |
c |    459112 |  113985   415808 |   89653   33162  2253530    68.0 | 25.560 % |
c |    462956 |  113985   415808 |   98619   37006  2469981    66.7 | 25.560 % |
c |    468722 |  113976   415777 |  108481   42767  2857456    66.8 | 25.564 % |
c |    477371 |  113967   415746 |  119329   51413  3638000    70.8 | 25.568 % |
c |    490345 |  113853   415352 |  131262   64371  5255429    81.6 | 25.629 % |
c |    509808 |  113813   415214 |  144388   83819  7382297    88.1 | 25.656 % |
c |    539001 |  113755   415016 |  158827  113007 10953547    96.9 | 25.695 % |
c ==============================================================================
c [1mFound solution: 1240224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 22   maxlim: 26778   bits: 16/15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    540625 |  113862   415421 |   37954  114631 11136741    97.2 | 25.695 % |
c |    540725 |  113798   415201 |   41749   27443  1780504    64.9 | 25.733 % |
c |    540875 |  113798   415201 |   45924   27593  1792658    65.0 | 25.733 % |
c |    541101 |  113751   415038 |   50516   27814  1795380    64.5 | 25.756 % |
c |    541438 |  113733   414974 |   55568   28147  1814067    64.4 | 25.760 % |
c |    541945 |  113661   414726 |   61125   28637  1820834    63.6 | 25.791 % |
c |    542706 |  113661   414726 |   67237   29398  1871224    63.7 | 25.791 % |
c |    543845 |  113661   414726 |   73961   30537  1967484    64.4 | 25.791 % |
c |    545555 |  113661   414726 |   81357   32247  2173326    67.4 | 25.791 % |
c |    548117 |  113652   414695 |   89493   34807  2394561    68.8 | 25.795 % |
c |    551965 |  113652   414695 |   98442   38655  3029577    78.4 | 25.795 % |
c |    557731 |  113589   414476 |  108287   44406  3582789    80.7 | 25.833 % |
c |    566383 |  113589   414476 |  119115   53058  4508122    85.0 | 25.833 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 x241_bit13 x242_bit0 -x243_bit0 -x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 x251_bit0 -x252_bit0 x253_bit0 x254_bit0 x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 x302_bit0 -x302_bit1 x303_bit0 -x303_bit1 -x304_bit0 -x304_bit1 -x305_bit0 -x305_bit1 -x306_bit0 -x306_bit1 -x307_bit0 -x307_bit1 -x308_bit0 -x308_bit1 -x309_bit0 -x309_bit1 -x310_bit0 -x310_bit1 -x311_bit0 -x311_bit1 -x312_bit0 -x312_bit1 -x313_bit0 -x313_bit1 -x314_bit0 -x314_bit1 -x315_bit0 -x315_bit1 -x316_bit0 -x316_bit1 -x317_bit0 -x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 -x354_bit0 -x355_bit0 -x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 x437_bit0 -x438_bit0 -x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 -x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 -x499_bit0 x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 -x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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_b#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.64 0.89 0.89 2/54 22017
Raw data (stat): 22017 (runsolver) R 22016 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546020969 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.70 0.90 0.89 2/54 22017
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 3232 0 0 0 991 7 0 0 25 0 1 0 546020969 15618048 3144 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3813 3144 603 41 0 3772 0
vsize: 15252
[startup+20.0011 s]
Raw data (loadavg): 0.74 0.90 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 3651 0 0 0 1989 9 0 0 25 0 1 0 546020969 17305600 3563 4294967295 134512640 134672761 3221224544 3221223792 134562140 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4225 3563 603 41 0 4184 0
vsize: 16900
[startup+30.001 s]
Raw data (loadavg): 0.78 0.90 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 3984 0 0 0 2987 10 0 0 25 0 1 0 546020969 18640896 3896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4551 3896 603 41 0 4510 0
vsize: 18204
[startup+40.0019 s]
Raw data (loadavg): 0.82 0.91 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 4252 0 0 0 3986 11 0 0 25 0 1 0 546020969 19849216 4164 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4846 4164 603 41 0 4805 0
vsize: 19384
[startup+50.0024 s]
Raw data (loadavg): 0.84 0.91 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 4503 0 0 0 4986 11 0 0 25 0 1 0 546020969 20922368 4415 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5108 4415 603 41 0 5067 0
vsize: 20432
[startup+60.0022 s]
Raw data (loadavg): 0.87 0.91 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 4762 0 0 0 5985 12 0 0 25 0 1 0 546020969 21991424 4674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5369 4674 603 41 0 5328 0
vsize: 21476
[startup+70.0033 s]
Raw data (loadavg): 0.89 0.91 0.89 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 4970 0 0 0 6985 13 0 0 25 0 1 0 546020969 22798336 4882 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5566 4882 603 41 0 5525 0
vsize: 22264
[startup+80.0038 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 5159 0 0 0 7984 14 0 0 25 0 1 0 546020969 23470080 5071 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5730 5071 603 41 0 5689 0
vsize: 22920
[startup+90.0047 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 5425 0 0 0 8983 15 0 0 25 0 1 0 546020969 24825856 5337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6061 5337 603 41 0 6020 0
vsize: 24244
[startup+100.005 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 5647 0 0 0 9983 15 0 0 25 0 1 0 546020969 25821184 5559 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6304 5559 603 41 0 6263 0
vsize: 25216
[startup+110.004 s]
Raw data (loadavg): 0.94 0.92 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 5810 0 0 0 10983 16 0 0 25 0 1 0 546020969 26492928 5722 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6468 5722 603 41 0 6427 0
vsize: 25872
[startup+120.005 s]
Raw data (loadavg): 0.95 0.92 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 5973 0 0 0 11983 16 0 0 25 0 1 0 546020969 27049984 5885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6604 5885 603 41 0 6563 0
vsize: 26416
[startup+130.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 6123 0 0 0 12983 17 0 0 25 0 1 0 546020969 27787264 6035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6784 6035 603 41 0 6743 0
vsize: 27136
[startup+140.006 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 6274 0 0 0 13982 17 0 0 25 0 1 0 546020969 28332032 6186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6917 6186 603 41 0 6876 0
vsize: 27668
[startup+150.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 6450 0 0 0 14982 18 0 0 25 0 1 0 546020969 29007872 6362 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7082 6362 603 41 0 7041 0
vsize: 28328
[startup+160.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 7300 0 0 0 15980 20 0 0 25 0 1 0 546020969 32505856 7212 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7936 7212 603 41 0 7895 0
vsize: 31744
[startup+170.007 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 7730 0 0 0 16979 22 0 0 25 0 1 0 546020969 34115584 7642 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8329 7642 603 41 0 8288 0
vsize: 33316
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 8154 0 0 0 17978 23 0 0 25 0 1 0 546020969 35864576 8066 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8756 8066 603 41 0 8715 0
vsize: 35024
[startup+190.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 8378 0 0 0 18976 24 0 0 25 0 1 0 546020969 37322752 8290 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9112 8290 603 41 0 9071 0
vsize: 36448
[startup+200.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 8550 0 0 0 19976 25 0 0 25 0 1 0 546020969 37986304 8462 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9274 8462 603 41 0 9233 0
vsize: 37096
[startup+210.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 8761 0 0 0 20976 25 0 0 25 0 1 0 546020969 38903808 8673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9498 8673 603 41 0 9457 0
vsize: 37992
[startup+220.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 8897 0 0 0 21976 25 0 0 25 0 1 0 546020969 39448576 8809 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9631 8809 603 41 0 9590 0
vsize: 38524
[startup+230.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9048 0 0 0 22975 26 0 0 25 0 1 0 546020969 39976960 8960 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9760 8960 603 41 0 9719 0
vsize: 39040
[startup+240.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9223 0 0 0 23975 26 0 0 25 0 1 0 546020969 40755200 9135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9950 9135 603 41 0 9909 0
vsize: 39800
[startup+250.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9373 0 0 0 24975 27 0 0 25 0 1 0 546020969 41422848 9285 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10113 9285 603 41 0 10072 0
vsize: 40452
[startup+260.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9517 0 0 0 25974 27 0 0 25 0 1 0 546020969 41963520 9429 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10245 9429 603 41 0 10204 0
vsize: 40980
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9688 0 0 0 26974 28 0 0 25 0 1 0 546020969 42631168 9600 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10408 9600 603 41 0 10367 0
vsize: 41632
[startup+280.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 9832 0 0 0 27974 28 0 0 25 0 1 0 546020969 43294720 9744 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10570 9744 603 41 0 10529 0
vsize: 42280
[startup+290.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 10132 0 0 0 28974 29 0 0 25 0 1 0 546020969 44511232 10044 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10867 10044 603 41 0 10826 0
vsize: 43468
[startup+300.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 10236 0 0 0 29974 30 0 0 25 0 1 0 546020969 44920832 10148 4294967295 134512640 134672761 3221224544 3221223712 134560966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10967 10148 603 41 0 10926 0
vsize: 43868
[startup+310.025 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 10444 0 0 0 30974 30 0 0 25 0 1 0 546020969 45723648 10356 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11163 10356 603 41 0 11122 0
vsize: 44652
[startup+320.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11143 0 0 0 31973 32 0 0 25 0 1 0 546020969 48537600 11055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11850 11055 603 41 0 11809 0
vsize: 47400
[startup+330.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 32972 33 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+340.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 33971 33 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+350.034 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 34971 33 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+360.035 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 35970 33 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+370.043 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 36971 33 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+380.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 37970 34 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+390.052 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 38970 34 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+400.058 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 39970 34 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+410.06 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 40970 34 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+420.06 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 41970 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223680 134565054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+430.067 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 42971 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+440.067 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 43970 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+450.067 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 44970 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+460.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 45972 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+470.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 46973 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+480.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 47973 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+490.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 48973 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+500.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11271 0 0 0 49974 35 0 0 25 0 1 0 546020969 49078272 11183 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11183 603 41 0 11941 0
vsize: 47928
[startup+510.092 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11278 0 0 0 50974 35 0 0 25 0 1 0 546020969 49078272 11190 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11190 603 41 0 11941 0
vsize: 47928
[startup+520.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11278 0 0 0 51974 36 0 0 25 0 1 0 546020969 49078272 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11190 603 41 0 11941 0
vsize: 47928
[startup+530.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11278 0 0 0 52975 36 0 0 25 0 1 0 546020969 49078272 11190 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11190 603 41 0 11941 0
vsize: 47928
[startup+540.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11400 0 0 0 53975 36 0 0 25 0 1 0 546020969 49602560 11312 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12110 11312 603 41 0 12069 0
vsize: 48440
[startup+550.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11651 0 0 0 54974 37 0 0 25 0 1 0 546020969 50548736 11563 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12341 11563 603 41 0 12300 0
vsize: 49364
[startup+560.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 11831 0 0 0 55974 37 0 0 25 0 1 0 546020969 51355648 11743 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12538 11743 603 41 0 12497 0
vsize: 50152
[startup+570.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12046 0 0 0 56974 38 0 0 25 0 1 0 546020969 52158464 11958 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12734 11958 603 41 0 12693 0
vsize: 50936
[startup+580.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12372 0 0 0 57973 38 0 0 25 0 1 0 546020969 53624832 12284 4294967295 134512640 134672761 3221224544 3221223472 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13092 12284 603 41 0 13051 0
vsize: 52368
[startup+590.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12617 0 0 0 58973 39 0 0 25 0 1 0 546020969 54611968 12529 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13333 12529 603 41 0 13292 0
vsize: 53332
[startup+600.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 59972 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+610.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 60973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+620.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 61973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+630.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 62973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+640.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 63973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+650.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 64973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+660.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 65973 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+670.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 66974 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+680.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 67974 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+690.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 68974 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+700.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 69974 39 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+710.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12645 0 0 0 70974 40 0 0 25 0 1 0 546020969 54820864 12557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12557 603 41 0 13343 0
vsize: 53536
[startup+720.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 71974 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+730.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 72974 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+740.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 73974 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+750.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 74975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+760.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 75975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223648 134560489 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+770.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 76975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+780.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 77975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+790.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 78975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+800.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 79975 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+810.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 80976 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+820.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 81976 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+830.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12647 0 0 0 82976 40 0 0 25 0 1 0 546020969 54820864 12559 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12559 603 41 0 13343 0
vsize: 53536
[startup+840.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12648 0 0 0 83976 40 0 0 25 0 1 0 546020969 54820864 12560 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12560 603 41 0 13343 0
vsize: 53536
[startup+850.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12648 0 0 0 84976 40 0 0 25 0 1 0 546020969 54820864 12560 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12560 603 41 0 13343 0
vsize: 53536
[startup+860.111 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12648 0 0 0 85976 40 0 0 25 0 1 0 546020969 54820864 12560 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12560 603 41 0 13343 0
vsize: 53536
[startup+870.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 86977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+880.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 87977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+890.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 88977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+900.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 89977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+910.112 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 90977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+920.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 91977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+930.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 92977 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+940.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 93978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+950.114 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 94978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+960.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 95978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+970.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 96978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223648 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+980.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 97978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+990.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12650 0 0 0 98978 40 0 0 25 0 1 0 546020969 54820864 12562 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12562 603 41 0 13343 0
vsize: 53536
[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 12879 0 0 0 99978 41 0 0 25 0 1 0 546020969 55750656 12791 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13611 12791 603 41 0 13570 0
vsize: 54444
[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 13210 0 0 0 100977 42 0 0 25 0 1 0 546020969 57085952 13122 4294967295 134512640 134672761 3221224544 3221223728 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13937 13122 603 41 0 13896 0
vsize: 55748
[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 13605 0 0 0 101976 43 0 0 25 0 1 0 546020969 58691584 13517 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14329 13517 603 41 0 14288 0
vsize: 57316
[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 13938 0 0 0 102975 44 0 0 25 0 1 0 546020969 60035072 13850 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 13850 603 41 0 14616 0
vsize: 58628
[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 14281 0 0 0 103975 45 0 0 25 0 1 0 546020969 61501440 14193 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15015 14193 603 41 0 14974 0
vsize: 60060
[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 14883 0 0 0 104973 47 0 0 25 0 1 0 546020969 63885312 14795 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15597 14795 603 41 0 15556 0
vsize: 62388
[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 15441 0 0 0 105972 47 0 0 25 0 1 0 546020969 66166784 15353 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16154 15353 603 41 0 16113 0
vsize: 64616
[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 16023 0 0 0 106971 49 0 0 25 0 1 0 546020969 68567040 15935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16740 15935 603 41 0 16699 0
vsize: 66960
[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 16446 0 0 0 107970 50 0 0 25 0 1 0 546020969 70311936 16358 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17166 16358 603 41 0 17125 0
vsize: 68664
[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 16884 0 0 0 108969 50 0 0 25 0 1 0 546020969 72052736 16796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17591 16796 603 41 0 17550 0
vsize: 70364
[startup+1100.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 109968 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 110969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 111969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 112969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 113969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 114969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 115969 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 116970 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 117970 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 118970 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22019
Raw data (stat): 22017 (minisat+) R 22016 11931 11930 0 -1 0 17113 0 0 0 119970 52 0 0 25 0 1 0 546020969 72982528 17025 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17818 17025 603 41 0 17777 0
vsize: 71272
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22019
Raw data (stat): 22017 (minisat+) Z 22016 11931 11930 0 -1 12 17116 0 0 0 119971 55 0 0 25 0 1 0 546020969 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.16
CPU time (s): 1200.27
CPU user time (s): 1199.71
CPU system time (s): 0.556915
CPU usage (%): 100.009
Max. virtual memory (Kb): 71272
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####