PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran6x43.opb
MD5SUM	795a1eda830447df9b9714fdf1d66b4e
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2795888
Optimality of the best value was proved	NO
Number of terms in the objective function	5418
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1537450315
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1537450315
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1224.65
Number of variables	5418
Total number of constraints	307
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	307
Minimum length of a constraint	21
Maximum length of a constraint	860
Trace number 17610

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        580040 kB
Buffers:         23724 kB
Cached:         409156 kB
SwapCached:        552 kB
Active:          47052 kB
Inactive:       387880 kB
HighTotal:      131008 kB
HighFree:         9436 kB
LowTotal:       903652 kB
LowFree:        570604 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            14104 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:12:08 (client local time) WITH STATUS 10 IN 1200.43 SECONDS
stats: 19354 7 1200.43 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 356 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 354]---> Adder-cost: 894   maxlim: 78677   bits: 17/17
c ---[ 352]---> Adder-cost: 894   maxlim: 84309   bits: 17/17
c ---[ 350]---> Adder-cost: 886   maxlim: 78933   bits: 17/17
c ---[ 348]---> Adder-cost: 894   maxlim: 93141   bits: 17/17
c ---[ 346]---> Adder-cost: 818   maxlim: 37973   bits: 16/16
c ---[ 344]---> Adder-cost: 894   maxlim: 84437   bits: 17/17
c ---[ 342]---> Adder-cost: 110   maxlim: 10234   bits: 14/14
c ---[ 340]---> Adder-cost: 100   maxlim: 5370   bits: 13/13
c ---[ 338]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[ 336]---> Adder-cost: 120   maxlim: 19066   bits: 15/15
c ---[ 334]---> Adder-cost: 120   maxlim: 19450   bits: 15/15
c ---[ 332]---> Adder-cost: 100   maxlim: 5370   bits: 13/13
c ---[ 330]---> Adder-cost: 90   maxlim: 2682   bits: 12/12
c ---[ 328]---> Adder-cost: 110   maxlim: 9594   bits: 14/14
c ---[ 326]---> Adder-cost: 128   maxlim: 33402   bits: 16/16
c ---[ 324]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[ 322]---> Adder-cost: 90   maxlim: 2810   bits: 12/12
c ---[ 320]---> Adder-cost: 110   maxlim: 10234   bits: 14/14
c ---[ 318]---> Adder-cost: 100   maxlim: 5498   bits: 13/13
c ---[ 316]---> Adder-cost: 128   maxlim: 31610   bits: 16/15
c ---[ 314]---> Adder-cost: 100   maxlim: 5370   bits: 13/13
c ---[ 312]---> Adder-cost: 90   maxlim: 2810   bits: 12/12
c ---[ 310]---> Adder-cost: 110   maxlim: 9850   bits: 14/14
c ---[ 308]---> Adder-cost: 100   maxlim: 5370   bits: 13/13
c ---[ 306]---> Adder-cost: 100   maxlim: 5242   bits: 13/13
c ---[ 304]---> Adder-cost: 90   maxlim: 2682   bits: 12/12
c ---[ 302]---> Adder-cost: 110   maxlim: 9338   bits: 14/14
c ---[ 300]---> Adder-cost: 120   maxlim: 19066   bits: 15/15
c ---[ 298]---> Adder-cost: 110   maxlim: 10234   bits: 14/14
c ---[ 296]---> Adder-cost: 100   maxlim: 5626   bits: 13/13
c ---[ 294]---> Adder-cost: 100   maxlim: 5626   bits: 13/13
c ---[ 292]---> Adder-cost: 100   maxlim: 5370   bits: 13/13
c ---[ 290]---> Adder-cost: 80   maxlim: 1402   bits: 11/11
c ---[ 288]---> Adder-cost: 90   maxlim: 2682   bits: 12/12
c ---[ 286]---> Adder-cost: 120   maxlim: 18554   bits: 15/15
c ---[ 284]---> Adder-cost: 90   maxlim: 2810   bits: 12/12
c ---[ 282]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[ 280]---> Adder-cost: 120   maxlim: 19322   bits: 15/15
c ---[ 278]---> Adder-cost: 128   maxlim: 33658   bits: 16/16
c ---[ 276]---> Adder-cost: 80   maxlim: 1402   bits: 11/11
c ---[ 274]---> Adder-cost: 120   maxlim: 18298   bits: 15/15
c ---[ 272]---> Adder-cost: 110   maxlim: 9594   bits: 14/14
c ---[ 270]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[ 268]---> Adder-cost: 90   maxlim: 2682   bits: 12/12
c ---[ 266]---> Adder-cost: 110   maxlim: 9978   bits: 14/14
c ---[ 264]---> Adder-cost: 128   maxlim: 33786   bits: 16/16
c ---[ 262]---> Adder-cost: 100   maxlim: 5626   bits: 13/13
c ---[ 260]---> Adder-cost: 100   maxlim: 5626   bits: 13/13
c ---[ 258]---> Adder-cost: 110   maxlim: 10234   bits: 14/14
c ---[ 257]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 256]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 255]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 254]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 253]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 252]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 251]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 250]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 249]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 248]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 247]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 246]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 245]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 244]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 243]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 242]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 241]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 240]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 239]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 238]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 237]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 236]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 234]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 233]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 232]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 231]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 230]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 228]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 227]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 226]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 225]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 224]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 223]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 220]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 217]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 216]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 215]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 214]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 212]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 211]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 210]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 209]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 208]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 207]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 206]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 204]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 203]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 202]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 4   maxlim: 8190   bits: 14/13
c ---[ 200]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 199]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 197]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 196]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 195]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 194]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 193]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 192]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 191]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 190]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 189]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 188]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 187]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 186]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 185]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 184]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 183]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 181]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 180]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 179]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 177]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 175]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 173]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 172]---> Adder-cost: 2   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: 2   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 166]---> Adder-cost: 2   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 ---[ 162]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 4   maxlim: 510   bits: 10/9
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: 2   maxlim: 2046   bits: 12/11
c ---[ 155]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 154]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 153]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 151]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 150]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 147]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 146]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 143]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 138]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 137]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 136]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 135]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 132]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 130]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 129]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 127]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 124]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 123]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 122]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 121]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 119]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 118]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 117]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 114]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 112]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 111]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 110]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 108]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 107]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 106]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 104]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 102]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 100]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  98]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  97]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  95]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  94]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  91]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  90]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  85]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  84]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  83]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  82]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  80]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  76]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  75]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  74]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  73]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  72]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  71]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  69]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  68]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  67]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  66]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  65]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  63]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  61]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  59]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  58]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[  54]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  53]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  48]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  47]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  45]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  43]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[  42]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  41]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  40]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  38]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  36]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  34]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  32]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  30]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  29]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  27]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  25]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  24]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  23]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  22]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  20]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  19]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  18]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  17]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  14]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  13]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  11]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   8]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   5]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   4]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[   2]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   1]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   73328   269896 |   24442       0        0     nan |  0.000 % |
c |       100 |   73328   269896 |   26886     100      282     2.8 | 33.044 % |
c |       250 |   73311   269837 |   29574     248      814     3.3 | 33.059 % |
c |       475 |   73281   269737 |   32532     470     1840     3.9 | 33.084 % |
c |       813 |   73272   269708 |   35785     807     3835     4.8 | 33.094 % |
c |      1319 |   73199   269463 |   39364    1306     6242     4.8 | 33.159 % |
c |      2079 |   72998   268788 |   43300    2038     9794     4.8 | 33.340 % |
c |      3219 |   72874   268370 |   47630    3163    15488     4.9 | 33.456 % |
c |      4927 |   72704   267804 |   52393    4848    24155     5.0 | 33.611 % |
c |      7489 |   72504   267126 |   57632    7386    37298     5.0 | 33.792 % |
c |     11333 |   72316   266492 |   63396   11209    57569     5.1 | 33.963 % |
c |     17099 |   71677   264325 |   69735   16882    89779     5.3 | 34.540 % |
c |     25748 |   71544   263886 |   76709   25514   164348     6.4 | 34.671 % |
c |     38722 |   71493   263713 |   84380   38475   344398     9.0 | 34.711 % |
c |     58184 |   71338   263200 |   92818   57917   609148    10.5 | 34.847 % |
c |     87376 |   71297   263065 |  102100   87104  1422586    16.3 | 34.887 % |
c |    131165 |   71273   262987 |  112310   42806  1060192    24.8 | 34.907 % |
c |    196849 |   71234   262856 |  123541  108484  2782461    25.6 | 34.942 % |
c |    295376 |   71109   262431 |  135895   96932  1868127    19.3 | 35.058 % |
c ==============================================================================
c [1mFound solution: 5333652[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10631   maxlim: 3153591   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    441220 |  145301   527425 |   48433  117319  4493635    38.3 | 35.058 % |
c |    441320 |  145301   527425 |   53276   25549   288002    11.3 | 22.918 % |
c |    441470 |  145301   527425 |   58603   25699   289251    11.3 | 22.918 % |
c |    441695 |  145301   527425 |   64464   25924   290366    11.2 | 22.918 % |
c |    442032 |  145301   527425 |   70910   26261   292165    11.1 | 22.918 % |
c |    442538 |  145301   527425 |   78001   26767   294732    11.0 | 22.918 % |
c |    443297 |  145275   527335 |   85802   27523   299458    10.9 | 22.931 % |
c |    444436 |  145275   527335 |   94382   28662   326518    11.4 | 22.931 % |
c |    446144 |  145275   527335 |  103820   30370   342994    11.3 | 22.931 % |
c |    448706 |  145275   527335 |  114202   32932   372816    11.3 | 22.931 % |
c |    452552 |  145275   527335 |  125622   36778   416498    11.3 | 22.931 % |
c |    458318 |  145275   527335 |  138185   42544   528640    12.4 | 22.931 % |
c |    466967 |  145275   527335 |  152003   51193   795479    15.5 | 22.931 % |
c |    479943 |  145275   527335 |  167203   64169  1128476    17.6 | 22.931 % |
c |    499404 |  145275   527335 |  183924   83630  1554563    18.6 | 22.931 % |
c |    528596 |  145275   527335 |  202316  112822  3639344    32.3 | 22.931 % |
c |    572385 |  145267   527309 |  222548  156610  5777348    36.9 | 22.934 % |
c ==============================================================================
c [1mFound solution: 5001306[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3485937   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    607412 |  145294   527509 |   48431  191637  7180804    37.5 | 22.934 % |
c |    607512 |  145294   527509 |   53274   22957   597850    26.0 | 22.956 % |
c |    607662 |  145294   527509 |   58601   23107   598448    25.9 | 22.956 % |
c |    607887 |  145294   527509 |   64461   23332   599481    25.7 | 22.956 % |
c |    608224 |  145294   527509 |   70907   23669   600996    25.4 | 22.956 % |
c |    608730 |  145294   527509 |   77998   24175   604343    25.0 | 22.956 % |
c |    609490 |  145294   527509 |   85798   24935   608548    24.4 | 22.956 % |
c |    610629 |  145294   527509 |   94378   26074   614317    23.6 | 22.956 % |
c |    612337 |  145294   527509 |  103816   27782   625788    22.5 | 22.956 % |
c |    614901 |  145294   527509 |  114197   30346   649810    21.4 | 22.956 % |
c |    618745 |  145294   527509 |  125617   34190   723051    21.1 | 22.956 % |
c |    624511 |  145294   527509 |  138179   39956   781244    19.6 | 22.956 % |
c |    633160 |  145294   527509 |  151997   48605  1041712    21.4 | 22.956 % |
c |    646135 |  145294   527509 |  167196   61580  1299862    21.1 | 22.956 % |
c |    665598 |  145294   527509 |  183916   81043  1615101    19.9 | 22.956 % |
c |    694791 |  145294   527509 |  202308  110236  2580481    23.4 | 22.956 % |
c |    738580 |  145294   527509 |  222539  154025  4483439    29.1 | 22.956 % |
c ==============================================================================
c [1mFound solution: 4988628[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3498615   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    774235 |  145305   527633 |   48435  189680  5538378    29.2 | 22.956 % |
c |    774335 |  145305   527633 |   53278   27374   505324    18.5 | 22.972 % |
c |    774485 |  145305   527633 |   58606   27524   505943    18.4 | 22.972 % |
c |    774710 |  145305   527633 |   64466   27749   507248    18.3 | 22.972 % |
c |    775047 |  145305   527633 |   70913   28086   508979    18.1 | 22.972 % |
c |    775553 |  145305   527633 |   78005   28592   511965    17.9 | 22.972 % |
c |    776312 |  145305   527633 |   85805   29351   516230    17.6 | 22.972 % |
c |    777451 |  145305   527633 |   94386   30490   522315    17.1 | 22.972 % |
c |    779159 |  145305   527633 |  103824   32198   535569    16.6 | 22.972 % |
c |    781721 |  145305   527633 |  114207   34760   552709    15.9 | 22.972 % |
c |    785567 |  145305   527633 |  125627   38606   601115    15.6 | 22.972 % |
c |    791333 |  145305   527633 |  138190   44372   702836    15.8 | 22.972 % |
c |    799982 |  145305   527633 |  152009   53021   882816    16.7 | 22.972 % |
c |    812957 |  145305   527633 |  167210   65996  1233855    18.7 | 22.972 % |
c |    832418 |  145305   527633 |  183931   85457  1792538    21.0 | 22.972 % |
c |    861610 |  145305   527633 |  202325  114649  2887676    25.2 | 22.972 % |
c ==============================================================================
c [1mFound solution: 4046447[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4440796   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    880066 |  145346   527912 |   48448  133105  3849454    28.9 | 22.972 % |
c |    880166 |  145346   527912 |   53292   26945   891904    33.1 | 22.997 % |
c |    880316 |  145346   527912 |   58622   27095   892578    32.9 | 22.997 % |
c |    880541 |  145346   527912 |   64484   27320   893577    32.7 | 22.997 % |
c |    880878 |  145346   527912 |   70932   27657   895310    32.4 | 22.997 % |
c |    881384 |  145346   527912 |   78025   28163   898112    31.9 | 22.997 % |
c |    882143 |  145346   527912 |   85828   28922   903703    31.2 | 22.997 % |
c |    883283 |  145346   527912 |   94411   30062   912035    30.3 | 22.997 % |
c |    884991 |  145346   527912 |  103852   31770   926055    29.1 | 22.997 % |
c |    887553 |  145346   527912 |  114237   34332   951908    27.7 | 22.997 % |
c |    891397 |  145346   527912 |  125661   38176   989501    25.9 | 22.997 % |
c |    897164 |  145346   527912 |  138227   43943  1112540    25.3 | 22.997 % |
c |    905814 |  145346   527912 |  152050   52593  1283207    24.4 | 22.997 % |
c |    918791 |  145346   527912 |  167255   65570  1481375    22.6 | 22.997 % |
c |    938253 |  145346   527912 |  183981   85032  2164344    25.5 | 22.997 % |
c |    967446 |  145346   527912 |  202379  114225  4457632    39.0 | 22.997 % |
c |   1011235 |  145346   527912 |  222617  158014  6181312    39.1 | 22.997 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 X0_bit_5 X0_bit_4 X0_bit_3 X0_bit_2 X0_bit_1 X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 X4_bit_7 X4_bit_6 X4_bit_5 X4_bit_4 X4_bit_3 X4_bit_2 X4_bit_1 -X4_bit0 X4_bit1 -X4_bit2 -X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 X5_bit_5 -X5_bit_4 X5_bit_3 X5_bit_2 -X5_bit_1 X5_bit0 X5_bit1 X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 X6_bit_7 X6_bit_6 X6_bit_5 -X6_bit_4 X6_bit_3 -X6_bit_2 X6_bit_1 X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 X8_bit_5 X8_bit_4 X8_bit_3 X8_bit_2 -X8_bit_1 X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 X9_bit_6 X9_bit_5 X9_bit_4 -X9_bit_3 X9_bit_2 -X9_bit_1 X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 X10_bit_6 X10_bit_5 X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 X10_bit0 X10_bit1 X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 X12_bit_2 -X12_bit_1 X12_bit0 -X12_bit1 -X12_bit2 X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 X13_bit_7 X13_bit_6 X13_bit_5 X13_bit_4 X13_bit_3 -X13_bit_2 -X13_bit_1 X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 X15_bit_6 X15_bit_5 X15_bit_4 X15_bit_3 -X15_bit_2 X15_bit_1 X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 X16_bit_7 X16_bit_6 X16_bit_5 X16_bit_4 X16_bit_3 X16_bit_2 X16_bit_1 X16_bit0 -X16_bit1 -X16_bit2 X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 X17_bit_6 -X17_bit_5 -X17_bit_4 X17_bit_3 X17_bit_2 -X17_bit_1 -X17_bit0 X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 X20_bit_6 X20_bit_5 X20_bit_4 X20_bit_3 X20_bit_2 X20_bit_1 X20_bit0 X20_bit1 X20_bit2 -X20_bit3 X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 X21_bit_7 X21_bit_6 X21_bit_5 X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 X23_bit_6 -X23_bit_5 X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 X24_bit_6 X24_bit_5 X24_bit_4 X24_bit_3 X24_bit_2 X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 X25_bit_7 X25_bit_6 X25_bit_5 X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 -X27_bit_6 -X27_bit_5 X27_bit_4 X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 X28_bit_6 X28_bit_5 -X28_bit_4 -X28_bit_3 X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 X30_bit_6 X30_bit_5 X30_bit_4 X30_bit_3 X30_bit_2 -X30_bit_1 X30_bit0 X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 X31_bit_6 X31_bit_5 X31_bit_4 X31_bit_3 -X31_bit_2 X31_bit_1 X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 X33_bit0 X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 X34_bit_6 -X34_bit_5 X34_bit_4 X34_bit_3 -X34_bit_2 X34_bit_1 X34_bit0 X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 X35_bit_6 X35_bit_5 X35_bit_4 X35_bit_3 X35_bit_2 X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 X36_bit_1 X36_bit0 X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 X37_bit_4 -X37_bit_3 -X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 X39_bit_5 -X39_bit_4 X39_bit_3 -X39_bit_2 X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 X40_bit_6 X40_bit_5 X40_bit_4 -X40_bit_3 -X40_bit_2 -X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 -X41_bit_5 -X41_bit_4 X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 X42_bit_2 X42_bit_1 -X42_bit0 X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 -X43_bit_6 X43_bit_5 X43_bit_4 X43_bit_3 X43_bit_2 X43_bit_1 X43_bit0 -X43_bit1 X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 X44_bit_4 X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 X46_bit_7 X46_bit_6 -X46_bit_5 X46_bit_4 X46_bit_3 X46_bit_2 -X46_bit_1 X46_bit0 X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 -X47_bit_6 X47_bit_5 X47_bit_4 X47_bit_3 X47_bit_2 X47_bit_1 -X47_bit0 X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 -X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 -X49_bit_6 -X49_bit_5 -X49_bit_4 -X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 X51_bit_3 X51_bit_2 -X51_bit_1 -X51_bit0 X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 X54_bit_4 -X54_bit_3 X54_bit_2 -X54_bit_1 -X54_bit0 X54_bit1 X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 X56_bit_6 X56_bit_5 X56_bit_4 X56_bit_3 X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 X57_bit_6 -X57_bit_5 X57_bit_4 X57_bit_3 X57_bit_2 -X57_bit_1 X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 X58_bit_7 X58_bit_6 X58_bit_5 X58_bit_4 X58_bit_3 -X58_bit_2 -X58_bit_1 X58_bit0 X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 X59_bit_6 X59_bit_5 X59_bit_4 X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 -X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 X61_bit_7 X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 X62_bit_7 X62_bit_6 X62_bit_5 -X62_bit_4 X62_bit_3 X62_bit_2 X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 X63_bit_6 X63_bit_5 X63_bit_4 X63_bit_3 X63_bit_2 X63_bit_1 -X63_bit0 X63_bit1 -X63_bit2 -X63_bit3 X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 X64_bit_6 X64_bit_5 -X64_bit_4 X64_bit_3 -X64_bit_2 -X64_bit_1 -X64_bit0 X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 -X65_bit_6 X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 X66_bit_6 -X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 X66_bit1 X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 X67_bit_6 X67_bit_5 X67_bit_4 X67_bit_3 X67_bit_2 X67_bit_1 -X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 X68_bit_5 X68_bit_4 -X68_bit_3 -X68_bit_2 X68_bit_1 -X68_bit0 -X68_bit1 X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 X69_bit_6 X69_bit_5 X69_bit_4 X69_bit_3 X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 X70_bit_7 X70_bit_6 -X70_bit_5 X70_bit_4 X70_bit_3 -X70_bit_2 X70_bit_1 X70_bit0 X70_bit1 X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 -X71_bit_5 -X71_bit_4 -X71_bit_3 -X71_bit_2 -X71_bit_1 -X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 -X72_bit_3 -X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 X73_bit_6 X73_bit_5 X73_bit_4 -X73_bit_3 X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 -X74_bit_6 X74_bit_5 -X74_bit_4 X74_bit_3 X74_bit_2 X74_bit_1 X74_bit0 X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 -X75_bit_7 X75_bit_6 -X75_bit_5 X75_bit_4 X75_bit_3 X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 -X77_bit_5 X77_bit_4 X77_bit_3 -X77_bit_2 -X77_bit_1 X77_bit0 X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 X79_bit_5 -X79_bit_4 -X79_bit_3 X79_bit_2 X79_bit_1 X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 X81_bit_5 X81_bit_4 X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 X81_bit2 -X81_bit3 X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 X84_bit_6 -X84_bit_5 X84_bit_4 X84_bit_3 X84_bit_2 X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 -X89_bit_7 X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 X91_bit_3 X91_bit_2 -X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 X92_bit_1 X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 X98_bit_6 X98_bit_5 -X98_bit_4 -X98_bit_3 X98_bit_2 -X98_bit_1 X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 X99_bit_6 X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 X100_bit_6 -X100_bit_5 X100_bit_4 X100_bit_3 X100_bit_2 -X100_bit_1 X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 -X101_bit_6 -X101_bit_5 -X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 X102_bit_7 X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 X102_bit_2 -X102_bit_1 -X102_bit0 X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 X103_bit_4 X103_bit_3 X103_bit_2 -X103_bit_1 X103_bit0 X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 X105_bit_6 X105_bit_5 -X105_bit_4 X105_bit_3 X105_bit_2 -X105_bit_1 -X105_bit0 X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 X106_bit_6 X106_bit_5 -X106_bit_4 X106_bit_3 X106_bit_2 X106_bit_1 -X106_bit0 X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 X108_bit_5 -X108_bit_4 X108_bit_3 X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 X109_bit_3 X109_bit_2 -X109_bit_1 X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 X112_bit_6 X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 X113_bit_2 X113_bit_1 -X113_bit0 X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 X114_bit_2 -X114_bit_1 -X114_bit0 X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 X120_bit_7 X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 X122_bit_4 -X122_bit_3 X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 X123_bit_7 X123_bit_6 X123_bit_5 X123_bit_4 -X123_bit_3 -X123_bit_2 X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 X124_bit_5 -X124_bit_4 -X124_bit_3 X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 X125_bit_5 X125_bit_4 -X125_bit_3 X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 -X126_bit_6 X126_bit_5 X126_bit_4 -X126_bit_3 X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 X131_bit_4 -X131_bit_3 -X131_bit_2 X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 X135_bit_6 -X135_bit_5 -X135_bit_4 X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 X140_bit1 X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 X145_bit_7 X145_bit_6 X145_bit_5 X145_bit_4 X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 X145_bit2 X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 -X146_bit_6 X146_bit_5 -X146_bit_4 X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 X148_bit_6 X148_bit_5 -X148_bit_4 X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 X150_bit_3 -X150_bit_2 -X150_bit_1 X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 -X151_bit_3 -X151_bit_2 -X151_bit_1 X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 X161_bit_4 -X161_bit_3 X161_bit_2 -X161_bit_1 -X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 X163_bit_1 X163_bit0 -X163_bit1 X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 X166_bit_6 -X166_bit_5 X166_bit_4 X166_bit_3 X166_bit_2 X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 X167_bit_2 -X167_bit_1 -X167_bit0 X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 X172_bit_7 X172_bit_6 X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 X174_bit_7 X174_bit_6 X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 X175_bit_7 X175_bit_6 -X175_bit_5 X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 X176_bit_7 X176_bit_6 X176_bit_5 X176_bit_4 -X176_bit_3 -X176_bit_2 -X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 X178_bit_6 X178_bit_5 X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 -X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 X180_bit_6 X180_bit_5 X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 X182_bit_6 -X182_bit_5 -X182_bit_4 X182_bit_3 -X182_bit_2 -X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 X185_bit_7 -X185_bit_6 X185_bit_5 X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 X186_bit_5 X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 X190_bit_4 X190_bit_3 -X190_bit_2 -X190_bit_1 X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 -X192_bit_6 X192_bit_5 X192_bit_4 X192_bit_3 X192_bit_2 X192_bit_1 X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 X193_bit_5 X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 X195_bit_5 X195_bit_4 X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 X197_bit_6 -X197_bit_5 -X197_bit_4 X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 -X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 X199_bit_6 -X199_bit_5 X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 X200_bit_6 -X200_bit_5 X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 X202_bit_6 -X202_bit_5 X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 X203_bit_5 X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 X204_bit_6 X204_bit_5 X204_bit_4 X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 -X208_bit_6 -X208_bit_5 -X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 -X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 X209_bit_7 -X209_bit_6 -X209_bit_5 X209_bit_4 -X209_bit_3 X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 -X211_bit_6 -X211_bit_5 -X211_bit_4 -X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 X216_bit_4 -X216_bit_3 X216_bit_2 X216_bit_1 X216_bit0 X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 X217_bit_6 X217_bit_5 X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 X219_bit_7 -X219_bit_6 X219_bit_5 -X219_bit_4 X219_bit_3 X219_bit_2 X219_bit_1 -X219_bit0 X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 X221_bit_6 -X221_bit_5 -X221_bit_4 X221_bit_3 X221_bit_2 -X221_bit_1 X221_bit0 X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 X224_bit_3 X224_bit_2 -X224_bit_1 -X224_bit0 X224_bit1 X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 X225_bit_2 X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 -X226_bit_6 -X226_bit_5 X226_bit_4 X226_bit_3 X226_bit_2 -X226_bit_1 -X226_bit0 X226_bit1 X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 X227_bit_4 X227_bit_3 X227_bit_2 -X227_bit_1 X227_bit0 -X227_bit1 X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 X228_bit_5 X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 -X230_bit_5 -X230_bit_4 -X230_bit_3 -X230_bit_2 -X230_bit_1 -X230_bit0 X230_bit1 X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 X231_bit_7 X231_bit_6 X231_bit_5 X231_bit_4 X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 X231_bit1 X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 -X233_bit_6 X233_bit_5 -X233_bit_4 -X233_bit_3 X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 X234_bit_7 X234_bit_6 X234_bit_5 -X234_bit_4 X234_bit_3 X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 X235_bit_6 X235_bit_5 X235_bit_4 X235_bit_3 X235_bit_2 X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 X236_bit_6 X236_bit_5 X236_bit_4 X236_bit_3 X236_bit_2 -X236_bit_1 -X236_bit0 X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 X241_bit_6 -X241_bit_5 X241_bit_4 X241_bit_3 X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 -X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 X249_bit_7 X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 X249_bit1 -X249_bit2 X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 -X250_bit_3 -X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 X251_bit_5 -X251_bit_4 X251_bit_3 X251_bit_2 -X251_bit_1 -X251_bit0 X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 X252_bit_7 X252_bit_6 X252_bit_5 X252_bit_4 X252_bit_3 X252_bit_2 -X252_bit_1 -X252_bit0 X252_bit1 -X252_bit2 X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 -X253_bit_6 -X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 X253_bit1 -X253_bit2 X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 -X254_bit_7 -X254_bit_6 -X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 X255_bit_6 -X255_bit_5 -X255_bit_4 X255_bit_3 -X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 X256_bit_7 -X256_bit_6 -X256_bit_5 -X256_bit_4 X256_bit_3 -X256_bit_2 -X256_bit_1 -X256_bit0 -X256_bit1 -X256_bit2 X256_bit3 -X256_bit4 -X256_bit5 -X256_bit6 -X256_bit7 -X256_bit8 -X256_bit9 -X256_bit10 -X256_bit11 -X256_bit12 -X257_bit_7 -X257_bit_6 -X257_bit_5 -X257_bit_4 -X257_bit_3 -X257_bit_2 -X257_bit_1 -X257_bit0 -X257_bit1 -X257_bit2 -X257_bit3 -X257_bit4 -X257_bit5 -X257_bit6 -X257_bit7 -X257_bit8 -X257_bit9 -X257_bit10 -X257_bit11 -X257_bit12 Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 -Y11_bit0 Y12_bit0 Y13_bit0 -Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 -Y19_bit0 Y20_bit0 Y21_bit0 Y22_bit0 Y23_bit0 Y24_bit0 Y25_bit0 -Y26_bit0 Y27_bit0 Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 -Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 Y37_bit0 -Y38_bit0 Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 Y43_bit0 Y44_bit0 -Y45_bit0 Y46_bit0 Y47_bit0 -Y48_bit0 -Y49_bit0 -Y50_bit0 Y51_bit0 -Y52_bit0 -Y53_bit0 Y54_bit0 -Y55_bit0 Y56_bit0 Y57_bit0 Y58_bit0 Y59_bit0 -Y60_bit0 Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 Y70_bit0 -Y71_bit0 -Y72_bit0 Y73_bit0 Y74_bit0 Y75_bit0 -Y76_bit0 Y77_bit0 -Y78_bit0 Y79_bit0 -Y80_bit0 Y81_bit0 -Y82_bit0 Y83_bit0 Y84_bit0 -Y85_bit0 -Y86_bit0 -Y87_bit0 Y88_bi#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.86 0.99 0.93 2/54 15267
Raw data (stat): 15267 (runsolver) R 15266 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486280970 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.88 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 2328 0 0 0 993 6 0 0 25 0 1 0 486280970 11939840 2253 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2915 2253 603 41 0 2874 0
vsize: 11660
[startup+20.0004 s]
Raw data (loadavg): 0.90 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 2411 0 0 0 1991 7 0 0 25 0 1 0 486280970 12210176 2336 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2336 603 41 0 2940 0
vsize: 11924
[startup+30.0002 s]
Raw data (loadavg): 0.92 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 2513 0 0 0 2992 7 0 0 25 0 1 0 486280970 12615680 2438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3080 2438 603 41 0 3039 0
vsize: 12320
[startup+39.9997 s]
Raw data (loadavg): 0.93 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 2721 0 0 0 3991 7 0 0 25 0 1 0 486280970 13422592 2646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3277 2646 603 41 0 3236 0
vsize: 13108
[startup+49.9999 s]
Raw data (loadavg): 0.94 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 2992 0 0 0 4991 8 0 0 25 0 1 0 486280970 14626816 2917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3571 2917 603 41 0 3530 0
vsize: 14284
[startup+59.9997 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 3099 0 0 0 5991 8 0 0 25 0 1 0 486280970 15032320 3024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3670 3024 603 41 0 3629 0
vsize: 14680
[startup+70.0001 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 3393 0 0 0 6990 9 0 0 25 0 1 0 486280970 16240640 3318 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3965 3318 603 41 0 3924 0
vsize: 15860
[startup+80.0003 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 3979 0 0 0 7989 11 0 0 25 0 1 0 486280970 18800640 3904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4590 3904 603 41 0 4549 0
vsize: 18360
[startup+90.0001 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 4441 0 0 0 8987 13 0 0 25 0 1 0 486280970 20688896 4366 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5051 4366 603 41 0 5010 0
vsize: 20204
[startup+99.9999 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 4729 0 0 0 9987 14 0 0 25 0 1 0 486280970 21766144 4654 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5314 4654 603 41 0 5273 0
vsize: 21256
[startup+110 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5266 0 0 0 10985 15 0 0 25 0 1 0 486280970 23920640 5191 4294967295 134512640 134672761 3221224544 3221223648 134559829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5840 5191 603 41 0 5799 0
vsize: 23360
[startup+120 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5558 0 0 0 11985 16 0 0 25 0 1 0 486280970 25133056 5483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6136 5483 603 41 0 6095 0
vsize: 24544
[startup+129.999 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5558 0 0 0 12985 16 0 0 25 0 1 0 486280970 25133056 5483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6136 5483 603 41 0 6095 0
vsize: 24544
[startup+139.999 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5558 0 0 0 13985 16 0 0 25 0 1 0 486280970 25133056 5483 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6136 5483 603 41 0 6095 0
vsize: 24544
[startup+149.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5558 0 0 0 14985 16 0 0 25 0 1 0 486280970 25133056 5483 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6136 5483 603 41 0 6095 0
vsize: 24544
[startup+159.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5558 0 0 0 15985 16 0 0 25 0 1 0 486280970 25133056 5483 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6136 5483 603 41 0 6095 0
vsize: 24544
[startup+169.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 5725 0 0 0 16985 17 0 0 25 0 1 0 486280970 25808896 5650 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6301 5650 603 41 0 6260 0
vsize: 25204
[startup+179.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 6210 0 0 0 17984 18 0 0 25 0 1 0 486280970 27824128 6135 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6793 6135 603 41 0 6752 0
vsize: 27172
[startup+189.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 6975 0 0 0 18983 20 0 0 25 0 1 0 486280970 30904320 6900 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7545 6900 603 41 0 7504 0
vsize: 30180
[startup+199.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7275 0 0 0 19982 21 0 0 25 0 1 0 486280970 32120832 7200 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7842 7200 603 41 0 7801 0
vsize: 31368
[startup+209.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 20981 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+219.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 21982 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+230 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 22982 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+239.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 23982 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+249.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 24983 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+259.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 25983 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+269.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 26983 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+279.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 27983 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+289.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7596 0 0 0 28984 22 0 0 25 0 1 0 486280970 33988608 7521 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8298 7521 603 41 0 8257 0
vsize: 33192
[startup+299.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 7819 0 0 0 29984 23 0 0 25 0 1 0 486280970 34795520 7744 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8495 7744 603 41 0 8454 0
vsize: 33980
[startup+309.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 8467 0 0 0 30982 24 0 0 25 0 1 0 486280970 37511168 8392 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9158 8392 603 41 0 9117 0
vsize: 36632
[startup+319.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9028 0 0 0 31982 25 0 0 25 0 1 0 486280970 39813120 8953 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9720 8953 603 41 0 9679 0
vsize: 38880
[startup+329.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 32980 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221221916 134566384 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+339.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 33980 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+349.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 34981 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+359.998 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 35981 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+369.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 36981 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+379.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 37982 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+389.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 38982 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+399.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 39982 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+409.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 40983 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+419.999 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 41983 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+430 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 9493 0 0 0 42983 27 0 0 25 0 1 0 486280970 41701376 9418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10181 9418 603 41 0 10140 0
vsize: 40724
[startup+440 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10389 0 0 0 43981 30 0 0 25 0 1 0 486280970 44994560 10231 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10985 10231 603 41 0 10944 0
vsize: 43940
[startup+450 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10389 0 0 0 44980 30 0 0 25 0 1 0 486280970 44994560 10231 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10231 603 41 0 10944 0
vsize: 43940
[startup+460 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10390 0 0 0 45980 30 0 0 25 0 1 0 486280970 44994560 10232 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10232 603 41 0 10944 0
vsize: 43940
[startup+470 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 15267
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10390 0 0 0 46981 30 0 0 25 0 1 0 486280970 44994560 10232 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10232 603 41 0 10944 0
vsize: 43940
[startup+480.003 s]
Raw data (loadavg): 0.99 0.99 0.93 4/58 15310
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10393 0 0 0 47981 30 0 0 25 0 1 0 486280970 44994560 10235 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10235 603 41 0 10944 0
vsize: 43940
[startup+490.003 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10393 0 0 0 48981 30 0 0 25 0 1 0 486280970 44994560 10235 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10235 603 41 0 10944 0
vsize: 43940
[startup+500.004 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 49982 30 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+510.004 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 50982 30 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+520.004 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 51982 31 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+530.004 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 52983 31 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+540.004 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 15320
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 53983 31 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+550.004 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10397 0 0 0 54983 31 0 0 25 0 1 0 486280970 44994560 10239 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10985 10239 603 41 0 10944 0
vsize: 43940
[startup+560.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 10637 0 0 0 55982 32 0 0 25 0 1 0 486280970 45932544 10479 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11214 10479 603 41 0 11173 0
vsize: 44856
[startup+570.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 11371 0 0 0 56980 34 0 0 25 0 1 0 486280970 49033216 11213 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11971 11213 603 41 0 11930 0
vsize: 47884
[startup+580.004 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 11911 0 0 0 57980 35 0 0 25 0 1 0 486280970 51208192 11753 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12502 11753 603 41 0 12461 0
vsize: 50008
[startup+590.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 12199 0 0 0 58980 35 0 0 25 0 1 0 486280970 52428800 12041 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12800 12041 603 41 0 12759 0
vsize: 51200
[startup+600.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 12559 0 0 0 59979 37 0 0 25 0 1 0 486280970 53911552 12401 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13162 12401 603 41 0 13121 0
vsize: 52648
[startup+610.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 12821 0 0 0 60978 37 0 0 25 0 1 0 486280970 54857728 12663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13393 12663 603 41 0 13352 0
vsize: 53572
[startup+620.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 13341 0 0 0 61977 39 0 0 25 0 1 0 486280970 57008128 13183 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13918 13183 603 41 0 13877 0
vsize: 55672
[startup+630.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 13821 0 0 0 62976 40 0 0 25 0 1 0 486280970 58892288 13663 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13663 603 41 0 14337 0
vsize: 57512
[startup+640.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 63975 41 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+650.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 64976 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+660.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 65976 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+670.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 66976 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+680.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 67977 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+690.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 68977 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+700.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 69977 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+710.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 70977 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+720.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 71978 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+730.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 72978 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+740.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 73978 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+750.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 74979 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223728 134559351 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+760.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 75979 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+770.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 76979 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+780.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 77979 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+790.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15322
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 78980 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+800.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 79980 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+810.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 80980 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+820.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 81981 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+830.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 82981 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223500 1075349796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+840.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 83981 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223744 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+850.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 84982 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+860.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 85982 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+870.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 86982 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+880.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 87983 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+890.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 88983 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+900.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 89983 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 90985 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+920.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 91986 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+930.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 92987 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+940.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 93987 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+950.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 94987 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+960.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 95988 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+970.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 96988 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134564732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+980.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 97988 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+990.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14157 0 0 0 98989 42 0 0 25 0 1 0 486280970 60219392 13994 4294967295 134512640 134672761 3221224544 3221223668 134566151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13994 603 41 0 14661 0
vsize: 58808
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 99989 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223724 134565156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 100989 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 101989 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 102990 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 103990 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 104991 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 105991 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 106991 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 107992 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 108992 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 109992 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 110993 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 111993 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 112993 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 113994 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 114994 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14159 0 0 0 115994 42 0 0 25 0 1 0 486280970 60219392 13996 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14702 13996 603 41 0 14661 0
vsize: 58808
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14253 0 0 0 116994 43 0 0 25 0 1 0 486280970 60624896 14090 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14801 14090 603 41 0 14760 0
vsize: 59204
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14438 0 0 0 117994 43 0 0 25 0 1 0 486280970 61435904 14275 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14999 14275 603 41 0 14958 0
vsize: 59996
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 14944 0 0 0 118993 45 0 0 25 0 1 0 486280970 63451136 14781 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15491 14781 603 41 0 15450 0
vsize: 61964
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 15324
Raw data (stat): 15267 (minisat+) R 15266 29653 29652 0 -1 0 15480 0 0 0 119992 47 0 0 25 0 1 0 486280970 65732608 15317 4294967295 134512640 134672761 3221224544 3221223728 134559512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16048 15317 603 41 0 16007 0
vsize: 64192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 15324
Raw data (stat): 15267 (minisat+) Z 15266 29653 29652 0 -1 12 15483 0 0 0 119993 50 0 0 25 0 1 0 486280970 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.43
CPU user time (s): 1199.93
CPU system time (s): 0.501923
CPU usage (%): 100.029
Max. virtual memory (Kb): 64192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####