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-ran4x64.opb
MD5SUM	6a6f7751d9c11fcafeb386712eac2f08
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3097606
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1473474440
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	1473474440
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	433.74
Number of variables	5376
Total number of constraints	324
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	324
Minimum length of a constraint	21
Maximum length of a constraint	1280
Trace number 14771

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        292280 kB
Buffers:         38112 kB
Cached:         662968 kB
SwapCached:          0 kB
Active:         245884 kB
Inactive:       458028 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        292028 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32836 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 01:35:20 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 19341 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 392 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 390]---> Adder-cost: 1332   maxlim: 117952   bits: 18/17
c ---[ 388]---> Adder-cost: 1332   maxlim: 118336   bits: 18/17
c ---[ 386]---> Adder-cost: 1332   maxlim: 115520   bits: 18/17
c ---[ 384]---> Adder-cost: 1332   maxlim: 91584   bits: 18/17
c ---[ 382]---> Adder-cost: 60   maxlim: 3324   bits: 12/12
c ---[ 380]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 378]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 376]---> Adder-cost: 78   maxlim: 27260   bits: 15/15
c ---[ 374]---> Adder-cost: 72   maxlim: 14076   bits: 14/14
c ---[ 372]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 370]---> Adder-cost: 66   maxlim: 6908   bits: 13/13
c ---[ 368]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 366]---> Adder-cost: 72   maxlim: 13692   bits: 14/14
c ---[ 364]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 362]---> Adder-cost: 66   maxlim: 6780   bits: 13/13
c ---[ 360]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 358]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 356]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 354]---> Adder-cost: 48   maxlim: 892   bits: 10/10
c ---[ 352]---> Adder-cost: 72   maxlim: 13308   bits: 14/14
c ---[ 350]---> Adder-cost: 78   maxlim: 27132   bits: 15/15
c ---[ 348]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 346]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 344]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 342]---> Adder-cost: 66   maxlim: 6780   bits: 13/13
c ---[ 340]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 338]---> Adder-cost: 66   maxlim: 6268   bits: 13/13
c ---[ 336]---> Adder-cost: 72   maxlim: 12540   bits: 14/14
c ---[ 334]---> Adder-cost: 66   maxlim: 6780   bits: 13/13
c ---[ 332]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 330]---> Adder-cost: 72   maxlim: 13948   bits: 14/14
c ---[ 328]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 326]---> Adder-cost: 48   maxlim: 892   bits: 10/10
c ---[ 324]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 322]---> Adder-cost: 66   maxlim: 7164   bits: 13/13
c ---[ 320]---> Adder-cost: 48   maxlim: 892   bits: 10/10
c ---[ 318]---> Adder-cost: 60   maxlim: 3324   bits: 12/12
c ---[ 316]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 314]---> Adder-cost: 66   maxlim: 6396   bits: 13/13
c ---[ 312]---> Adder-cost: 60   maxlim: 3324   bits: 12/12
c ---[ 310]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 308]---> Adder-cost: 60   maxlim: 3196   bits: 12/12
c ---[ 306]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 304]---> Adder-cost: 66   maxlim: 7036   bits: 13/13
c ---[ 302]---> Adder-cost: 72   maxlim: 13564   bits: 14/14
c ---[ 300]---> Adder-cost: 72   maxlim: 12412   bits: 14/14
c ---[ 298]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 296]---> Adder-cost: 66   maxlim: 7036   bits: 13/13
c ---[ 294]---> Adder-cost: 66   maxlim: 6652   bits: 13/13
c ---[ 292]---> Adder-cost: 78   maxlim: 28668   bits: 15/15
c ---[ 290]---> Adder-cost: 60   maxlim: 3452   bits: 12/12
c ---[ 288]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 286]---> Adder-cost: 60   maxlim: 3196   bits: 12/12
c ---[ 284]---> Adder-cost: 66   maxlim: 6780   bits: 13/13
c ---[ 282]---> Adder-cost: 78   maxlim: 28540   bits: 15/15
c ---[ 280]---> Adder-cost: 72   maxlim: 14204   bits: 14/14
c ---[ 278]---> Adder-cost: 66   maxlim: 6268   bits: 13/13
c ---[ 276]---> Adder-cost: 54   maxlim: 1660   bits: 11/11
c ---[ 274]---> Adder-cost: 60   maxlim: 3452   bits: 12/12
c ---[ 272]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 270]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 268]---> Adder-cost: 60   maxlim: 3580   bits: 12/12
c ---[ 266]---> Adder-cost: 72   maxlim: 14204   bits: 14/14
c ---[ 264]---> Adder-cost: 60   maxlim: 3196   bits: 12/12
c ---[ 262]---> Adder-cost: 66   maxlim: 6268   bits: 13/13
c ---[ 260]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 258]---> Adder-cost: 60   maxlim: 3196   bits: 12/12
c ---[ 256]---> Adder-cost: 54   maxlim: 1788   bits: 11/11
c ---[ 255]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 254]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 253]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 252]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 251]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 250]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 249]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 247]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 246]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 245]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 244]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 243]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 242]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 241]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 240]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 239]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 237]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 236]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 234]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 233]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 232]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 231]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 230]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 228]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 224]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 219]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 218]---> Adder-cost: 8   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: 510   bits: 10/9
c ---[ 214]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 213]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 211]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 210]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 209]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 208]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 204]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 203]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 202]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 200]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 199]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 198]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 197]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 196]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 195]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 194]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 193]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 192]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 188]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 187]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 186]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 185]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 184]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 183]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 182]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 181]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 180]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 179]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 178]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 176]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 175]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 173]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 172]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 171]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 170]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 169]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 167]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 166]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 165]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 164]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 163]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 162]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 161]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 160]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 159]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 158]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 156]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 155]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 154]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 153]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 151]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 150]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 149]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 148]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 147]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 145]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 144]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 143]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 139]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 138]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 136]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 133]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 132]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 130]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 128]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 127]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 126]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 125]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 124]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 123]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 121]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 119]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 118]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 115]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 114]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 113]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 112]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 111]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 110]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 109]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 108]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 107]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 106]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 105]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 104]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 102]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 100]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  99]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  97]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  95]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  92]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  91]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  90]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  88]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  82]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  80]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  77]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  76]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  70]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  68]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  67]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  64]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  63]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  62]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  61]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  60]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  59]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  58]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  57]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  56]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  54]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[  53]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  48]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  47]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  45]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  41]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  40]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  34]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[  32]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  31]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  30]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  29]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  27]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  26]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  25]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  23]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  20]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  19]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  18]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  16]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  15]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  14]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  13]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[  12]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  11]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  10]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   9]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   8]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   4]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   0]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   69568   256036 |   23189       0        0     nan |  0.000 % |
c |       100 |   69568   256036 |   25507     100      273     2.7 | 34.841 % |
c |       250 |   69568   256036 |   28058     250      940     3.8 | 34.841 % |
c |       475 |   69508   255840 |   30864     464     1826     3.9 | 34.893 % |
c |       812 |   69474   255730 |   33951     796     2957     3.7 | 34.929 % |
c |      1318 |   69316   255220 |   37346    1281     5115     4.0 | 35.077 % |
c |      2077 |   69007   254223 |   41080    2001     7898     3.9 | 35.375 % |
c |      3216 |   68813   253593 |   45188    3115    12295     3.9 | 35.565 % |
c |      4924 |   68674   253136 |   49707    4803    19699     4.1 | 35.693 % |
c |      7486 |   68617   252951 |   54678    7358    38909     5.3 | 35.749 % |
c |     11330 |   68560   252766 |   60146   11195   123971    11.1 | 35.806 % |
c |     17096 |   68471   252481 |   66160   16950   294262    17.4 | 35.893 % |
c |     25745 |   68420   252316 |   72777   25592   414637    16.2 | 35.944 % |
c |     38719 |   68363   252131 |   80054   38559   655467    17.0 | 35.996 % |
c |     58180 |   68363   252131 |   88060   58020  1292974    22.3 | 35.996 % |
c |     87372 |   68354   252102 |   96866   87211  2444891    28.0 | 36.006 % |
c |    131161 |   68354   252102 |  106552   48621  1248928    25.7 | 36.006 % |
c |    196846 |   68346   252076 |  117208  114305  3248255    28.4 | 36.011 % |
c |    295372 |   68346   252076 |  128928  106623  6165598    57.8 | 36.011 % |
c |    443161 |   68329   252015 |  141821   23214  1286686    55.4 | 36.021 % |
c ==============================================================================
c [1mFound solution: 5702241[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10520   maxlim: 2677543   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    649710 |  141865   514686 |   47288  104704  1758352    16.8 | 36.021 % |
c |    649810 |  141865   514686 |   52016   25816   302354    11.7 | 23.430 % |
c |    649960 |  141865   514686 |   57218   25966   303051    11.7 | 23.430 % |
c |    650185 |  141865   514686 |   62940   26191   304093    11.6 | 23.430 % |
c |    650522 |  141865   514686 |   69234   26528   306015    11.5 | 23.430 % |
c |    651029 |  141865   514686 |   76157   27035   308595    11.4 | 23.430 % |
c |    651788 |  141865   514686 |   83773   27794   313653    11.3 | 23.430 % |
c |    652927 |  141865   514686 |   92150   28933   320200    11.1 | 23.430 % |
c |    654635 |  141865   514686 |  101366   30641   340496    11.1 | 23.430 % |
c |    657198 |  141865   514686 |  111502   33204   370200    11.1 | 23.430 % |
c |    661044 |  141865   514686 |  122652   37050   424360    11.5 | 23.430 % |
c |    666810 |  141865   514686 |  134918   42816   510373    11.9 | 23.430 % |
c |    675459 |  141865   514686 |  148410   51465   719165    14.0 | 23.430 % |
c |    688433 |  141865   514686 |  163251   64439   952625    14.8 | 23.430 % |
c ==============================================================================
c [1mFound solution: 5587117[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 2792667   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    695063 |  141898   514923 |   47299   71069  1069826    15.1 | 23.430 % |
c |    695163 |  141898   514923 |   52028   25715   217596     8.5 | 23.454 % |
c |    695313 |  141898   514923 |   57231   25865   218256     8.4 | 23.454 % |
c |    695539 |  141898   514923 |   62954   26091   219381     8.4 | 23.454 % |
c |    695876 |  141898   514923 |   69250   26428   221368     8.4 | 23.454 % |
c |    696383 |  141898   514923 |   76175   26935   227644     8.5 | 23.454 % |
c |    697142 |  141898   514923 |   83793   27694   237505     8.6 | 23.454 % |
c |    698281 |  141898   514923 |   92172   28833   260776     9.0 | 23.454 % |
c |    699990 |  141898   514923 |  101389   30542   307751    10.1 | 23.454 % |
c |    702554 |  141898   514923 |  111528   33106   355461    10.7 | 23.454 % |
c |    706398 |  141898   514923 |  122681   36950   420506    11.4 | 23.454 % |
c |    712164 |  141898   514923 |  134949   42716   518373    12.1 | 23.454 % |
c |    720814 |  141898   514923 |  148444   51366   757964    14.8 | 23.454 % |
c |    733789 |  141898   514923 |  163288   64341   988123    15.4 | 23.454 % |
c ==============================================================================
c [1mFound solution: 5310517[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3069267   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    747288 |  141916   515081 |   47305   77840  1135547    14.6 | 23.454 % |
c |    747388 |  141916   515081 |   52035   24943   168178     6.7 | 23.477 % |
c |    747539 |  141916   515081 |   57239   25094   168955     6.7 | 23.477 % |
c |    747766 |  141916   515081 |   62962   25321   170269     6.7 | 23.477 % |
c |    748103 |  141916   515081 |   69259   25658   172992     6.7 | 23.477 % |
c |    748609 |  141916   515081 |   76185   26164   177518     6.8 | 23.477 % |
c |    749368 |  141916   515081 |   83803   26923   185893     6.9 | 23.477 % |
c |    750508 |  141916   515081 |   92184   28063   215477     7.7 | 23.477 % |
c |    752216 |  141916   515081 |  101402   29771   231507     7.8 | 23.477 % |
c |    754781 |  141916   515081 |  111542   32336   254756     7.9 | 23.477 % |
c |    758625 |  141916   515081 |  122696   36180   434742    12.0 | 23.477 % |
c |    764391 |  141916   515081 |  134966   41946   483684    11.5 | 23.477 % |
c |    773041 |  141916   515081 |  148463   50596   947612    18.7 | 23.477 % |
c |    786015 |  141916   515081 |  163309   63570  1640449    25.8 | 23.477 % |
c |    805476 |  141916   515081 |  179640   83031  2044904    24.6 | 23.477 % |
c |    834669 |  141916   515081 |  197604  112224  3792983    33.8 | 23.477 % |
c |    878459 |  141916   515081 |  217365  156014  5352132    34.3 | 23.477 % |
c ==============================================================================
c [1mFound solution: 4369417[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4010367   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    896321 |  141934   515198 |   47311  173876  5879315    33.8 | 23.477 % |
c |    896421 |  141934   515198 |   52042   27475   476881    17.4 | 23.497 % |
c |    896571 |  141934   515198 |   57246   27625   477530    17.3 | 23.497 % |
c |    896796 |  141934   515198 |   62970   27850   478604    17.2 | 23.497 % |
c |    897134 |  141934   515198 |   69268   28188   480152    17.0 | 23.497 % |
c |    897640 |  141934   515198 |   76194   28694   482424    16.8 | 23.497 % |
c |    898399 |  141934   515198 |   83814   29453   486135    16.5 | 23.497 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 X4_bit_2 X4_bit_1 -X4_bit0 -X4_bit1 X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 X8_bit_6 -X8_bit_5 X8_bit_4 X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 -X10_bit_5 X10_bit_4 X10_bit_3 X10_bit_2 X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 X13_bit_4 X13_bit_3 X13_bit_2 X13_bit_1 X13_bit0 X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 X14_bit_3 X14_bit_2 X14_bit_1 X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X15_bit_7 -X15_bit_6 X15_bit_5 X15_bit_4 X15_bit_3 -X15_bit_2 X15_bit_1 -X15_bit0 X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 X16_bit_2 X16_bit_1 -X16_bit0 -X16_bit1 X16_bit2 X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 -X17_bit_6 -X17_bit_5 X17_bit_4 X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 X19_bit_5 X19_bit_4 X19_bit_3 X19_bit_2 -X19_bit_1 X19_bit0 -X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 X20_bit_3 X20_bit_2 -X20_bit_1 X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 X22_bit_7 X22_bit_6 X22_bit_5 X22_bit_4 X22_bit_3 X22_bit_2 -X22_bit_1 -X22_bit0 X22_bit1 X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 X23_bit_6 X23_bit_5 X23_bit_4 -X23_bit_3 X23_bit_2 X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 X26_bit_5 X26_bit_4 -X26_bit_3 -X26_bit_2 X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 X29_bit_7 X29_bit_6 X29_bit_5 X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 X29_bit1 X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 X30_bit_7 -X30_bit_6 X30_bit_5 X30_bit_4 X30_bit_3 X30_bit_2 X30_bit_1 X30_bit0 X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 X31_bit_7 X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 X33_bit_6 X33_bit_5 -X33_bit_4 X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 X34_bit_7 -X34_bit_6 X34_bit_5 X34_bit_4 X34_bit_3 -X34_bit_2 X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 X35_bit_7 X35_bit_6 X35_bit_5 -X35_bit_4 X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 X36_bit_6 X36_bit_5 X36_bit_4 X36_bit_3 X36_bit_2 X36_bit_1 X36_bit0 X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 X38_bit_3 X38_bit_2 X38_bit_1 X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 X39_bit_6 -X39_bit_5 X39_bit_4 X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 X40_bit_6 -X40_bit_5 -X40_bit_4 X40_bit_3 -X40_bit_2 X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 X42_bit_3 X42_bit_2 X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 -X43_bit0 -X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 -X44_bit_6 -X44_bit_5 X44_bit_4 X44_bit_3 X44_bit_2 X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 X45_bit_1 -X45_bit0 X45_bit1 X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 X46_bit_3 X46_bit_2 X46_bit_1 X46_bit0 X46_bit1 X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 -X47_bit_5 X47_bit_4 X47_bit_3 -X47_bit_2 X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 -X48_bit_6 X48_bit_5 -X48_bit_4 X48_bit_3 -X48_bit_2 -X48_bit_1 X48_bit0 X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 X49_bit_5 X49_bit_4 -X49_bit_3 -X49_bit_2 X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 -X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 X52_bit_7 X52_bit_6 X52_bit_5 X52_bit_4 X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 X54_bit_7 X54_bit_6 X54_bit_5 X54_bit_4 X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 X55_bit_7 -X55_bit_6 X55_bit_5 X55_bit_4 X55_bit_3 X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 X56_bit_1 X56_bit0 X56_bit1 X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 X58_bit_6 X58_bit_5 -X58_bit_4 X58_bit_3 -X58_bit_2 -X58_bit_1 X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 X59_bit_6 -X59_bit_5 X59_bit_4 X59_bit_3 X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 X60_bit_6 X60_bit_5 -X60_bit_4 -X60_bit_3 X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 X63_bit_5 -X63_bit_4 X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 X63_bit1 X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 -X64_bit_7 -X64_bit_6 -X64_bit_5 -X64_bit_4 -X64_bit_3 -X64_bit_2 X64_bit_1 X64_bit0 X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 -X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 -X67_bit_7 -X67_bit_6 -X67_bit_5 -X67_bit_4 -X67_bit_3 -X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 -X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 -X72_bit_7 X72_bit_6 -X72_bit_5 X72_bit_4 X72_bit_3 X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 -X75_bit_6 -X75_bit_5 -X75_bit_4 -X75_bit_3 -X75_bit_2 -X75_bit_1 X75_bit0 X75_bit1 -X75_bit2 X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 X76_bit_6 X76_bit_5 X76_bit_4 X76_bit_3 -X76_bit_2 X76_bit_1 -X76_bit0 X76_bit1 -X76_bit2 X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 -X77_bit_6 -X77_bit_5 X77_bit_4 X77_bit_3 X77_bit_2 -X77_bit_1 X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 -X78_bit_6 X78_bit_5 -X78_bit_4 X78_bit_3 X78_bit_2 X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 X79_bit_7 -X79_bit_6 X79_bit_5 X79_bit_4 X79_bit_3 -X79_bit_2 X79_bit_1 X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 X81_bit_7 -X81_bit_6 -X81_bit_5 X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 X82_bit_2 -X82_bit_1 X82_bit0 -X82_bit1 X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 X83_bit_7 X83_bit_6 X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 X85_bit_5 X85_bit_4 X85_bit_3 -X85_bit_2 X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 X87_bit_6 X87_bit_5 X87_bit_4 X87_bit_3 X87_bit_2 X87_bit_1 X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 X89_bit_5 X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 -X91_bit_6 -X91_bit_5 -X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 X91_bit0 X91_bit1 -X91_bit2 X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 -X92_bit_7 X92_bit_6 -X92_bit_5 X92_bit_4 -X92_bit_3 X92_bit_2 -X92_bit_1 X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 X93_bit_6 X93_bit_5 X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 X94_bit_6 X94_bit_5 X94_bit_4 X94_bit_3 X94_bit_2 X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 -X95_bit_6 -X95_bit_5 X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 -X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 X97_bit_7 X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 -X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bit_6 -X99_bit_5 -X99_bit_4 X99_bit_3 X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 X100_bit_6 X100_bit_5 X100_bit_4 X100_bit_3 -X100_bit_2 X100_bit_1 X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 X101_bit_6 -X101_bit_5 X101_bit_4 X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 X104_bit_6 -X104_bit_5 -X104_bit_4 X104_bit_3 X104_bit_2 -X104_bit_1 X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 X106_bit_6 X106_bit_5 X106_bit_4 X106_bit_3 X106_bit_2 X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 -X107_bit_5 X107_bit_4 X107_bit_3 X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 X109_bit_7 -X109_bit_6 -X109_bit_5 X109_bit_4 -X109_bit_3 -X109_bit_2 X109_bit_1 X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 X110_bit_6 X110_bit_5 -X110_bit_4 -X110_bit_3 X110_bit_2 X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 -X111_bit_6 -X111_bit_5 X111_bit_4 -X111_bit_3 X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 X116_bit_5 X116_bit_4 X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 -X118_bit_6 X118_bit_5 X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 -X119_bit_7 -X119_bit_6 X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 X122_bit_6 X122_bit_5 X122_bit_4 -X122_bit_3 X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 X124_bit_7 -X124_bit_6 X124_bit_5 X124_bit_4 X124_bit_3 X124_bit_2 X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 X125_bit_1 -X125_bit0 X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 X126_bit_2 X126_bit_1 X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 -X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 X140_bit_6 -X140_bit_5 -X140_bit_4 -X140_bit_3 X140_bit_2 -X140_bit_1 X140_bit0 X140_bit1 X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 X141_bit_3 X141_bit_2 -X141_bit_1 X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 X142_bit0 X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 X144_bit_2 -X144_bit_1 -X144_bit0 X144_bit1 X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 X145_bit_7 -X145_bit_6 -X145_bit_5 -X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 -X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 X147_bit_3 X147_bit_2 X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 X148_bit_3 X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 X150_bit_7 X150_bit_6 -X150_bit_5 -X150_bit_4 X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 X151_bit_3 -X151_bit_2 -X151_bit_1 -X151_bit0 X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 X153_bit_7 X153_bit_6 X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 X153_bit_1 -X153_bit0 X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 X156_bit_6 X156_bit_5 -X156_bit_4 X156_bit_3 -X156_bit_2 X156_bit_1 X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 X157_bit_7 X157_bit_6 X157_bit_5 -X157_bit_4 X157_bit_3 -X157_bit_2 X157_bit_1 X157_bit0 X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 X158_bit_7 X158_bit_6 X158_bit_5 -X158_bit_4 X158_bit_3 -X158_bit_2 -X158_bit_1 X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 X159_bit_5 -X159_bit_4 X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 -X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 X161_bit_7 X161_bit_6 X161_bit_5 -X161_bit_4 -X161_bit_3 X161_bit_2 -X161_bit_1 X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 X162_bit_7 X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 X165_bit_3 X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 X166_bit_3 X166_bit_2 X166_bit_1 -X166_bit0 X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 X170_bit_7 -X170_bit_6 X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 X170_bit_1 -X170_bit0 X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 X173_bit_6 X173_bit_5 -X173_bit_4 X173_bit_3 X173_bit_2 X173_bit_1 X173_bit0 -X173_bit1 X173_bit2 X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 X174_bit_6 -X174_bit_5 -X174_bit_4 X174_bit_3 X174_bit_2 X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 X175_bit_7 X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 X176_bit_7 X176_bit_6 -X176_bit_5 -X176_bit_4 X176_bit_3 X176_bit_2 -X176_bit_1 X176_bit0 X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 X177_bit_6 -X177_bit_5 -X177_bit_4 X177_bit_3 X177_bit_2 -X177_bit_1 X177_bit0 X177_bit1 -X177_bit2 X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 -X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 X181_bit_2 -X181_bit_1 X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 X182_bit_7 X182_bit_6 X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 -X184_bit_6 -X184_bit_5 -X184_bit_4 -X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 X185_bit_7 X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 X187_bit_6 X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 X188_bit_5 -X188_bit_4 X188_bit_3 X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 X189_bit_1 -X189_bit0 X189_bit1 X189_bit2 X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 X190_bit_5 -X190_bit_4 X190_bit_3 X190_bit_2 X190_bit_1 -X190_bit0 X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 X191_bit_2 -X191_bit_1 -X191_bit0 X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 X192_bit_1 -X192_bit0 X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 X195_bit_7 X195_bit_6 X195_bit_5 X195_bit_4 X195_bit_3 X195_bit_2 X195_bit_1 X195_bit0 X195_bit1 -X195_bit2 X195_bit3 X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 X196_bit_7 -X196_bit_6 X196_bit_5 X196_bit_4 X196_bit_3 -X196_bit_2 -X196_bit_1 X196_bit0 -X196_bit1 -X196_bit2 X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 -X197_bit_5 -X197_bit_4 -X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 -X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 X200_bit_5 X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 X203_bit_7 X203_bit_6 X203_bit_5 X203_bit_4 X203_bit_3 X203_bit_2 X203_bit_1 X203_bit0 X203_bit1 X203_bit2 X203_bit3 X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 X205_bit_6 X205_bit_5 X205_bit_4 X205_bit_3 -X205_bit_2 -X205_bit_1 X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 X206_bit_6 X206_bit_5 -X206_bit_4 X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 X207_bit_7 -X207_bit_6 X207_bit_5 -X207_bit_4 -X207_bit_3 X207_bit_2 -X207_bit_1 X207_bit0 X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 -X208_bit_6 X208_bit_5 X208_bit_4 X208_bit_3 X208_bit_2 X208_bit_1 X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 X209_bit_7 -X209_bit_6 X209_bit_5 X209_bit_4 X209_bit_3 -X209_bit_2 X209_bit_1 X209_bit0 X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 X210_bit_5 X210_bit_4 X210_bit_3 -X210_bit_2 X210_bit_1 X210_bit0 X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 X211_bit_7 X211_bit_6 -X211_bit_5 X211_bit_4 -X211_bit_3 -X211_bit_2 X211_bit_1 -X211_bit0 -X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 X212_bit_6 X212_bit_5 X212_bit_4 X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 X213_bit_5 -X213_bit_4 -X213_bit_3 X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 X214_bit_6 X214_bit_5 X214_bit_4 -X214_bit_3 X214_bit_2 -X214_bit_1 X214_bit0 X214_bit1 X214_bit2 X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 X215_bit0 X215_bit1 X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 -X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 X216_bit0 X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 X217_bit_5 X217_bit_4 -X217_bit_3 X217_bit_2 -X217_bit_1 X217_bit0 X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 X218_bit_5 -X218_bit_4 X218_bit_3 X218_bit_2 -X218_bit_1 -X218_bit0 X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 -X221_bit_6 X221_bit_5 X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 X221_bit0 X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 X222_bit_7 -X222_bit_6 X222_bit_5 X222_bit_4 -X222_bit_3 X222_bit_2 X222_bit_1 X222_bit0 X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 X223_bit_2 X223_bit_1 X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 X224_bit0 X224_bit1 -X224_bit2 -X224_bit3 X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 X225_bit_7 X225_bit_6 X225_bit_5 X225_bit_4 X225_bit_3 X225_bit_2 -X225_bit_1 -X225_bit0 X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 -X226_bit_6 -X226_bit_5 -X226_bit_4 -X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 X227_bit_6 X227_bit_5 -X227_bit_4 X227_bit_3 X227_bit_2 -X227_bit_1 X227_bit0 X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 X228_bit_5 -X228_bit_4 -X228_bit_3 X228_bit_2 X228_bit_1 X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 -X229_bit_6 X229_bit_5 -X229_bit_4 X229_bit_3 X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 X230_bit_5 X230_bit_4 X230_bit_3 -X230_bit_2 X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 X231_bit_5 -X231_bit_4 X231_bit_3 -X231_bit_2 X231_bit_1 X231_bit0 X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 X232_bit_5 X232_bit_4 -X232_bit_3 X232_bit_2 X232_bit_1 X232_bit0 X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 -X233_bit_5 -X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 X234_bit_6 X234_bit_5 X234_bit_4 X234_bit_3 X234_bit_2 -X234_bit_1 -X234_bit0 X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 X235_bit_4 -X235_bit_3 -X235_bit_2 X235_bit_1 -X235_bit0 X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 X236_bit_7 X236_bit_6 X236_bit_5 X236_bit_4 X236_bit_3 X236_bit_2 X236_bit_1 X236_bit0 X236_bit1 X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 X238_bit_4 X238_bit_3 X238_bit_2 -X238_bit_1 X238_bit0 -X238_bit1 X238_bit2 -X238_bit3 X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 X239_bit_7 -X239_bit_6 -X239_bit_5 X239_bit_4 X239_bit_3 X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 X240_bit_7 -X240_bit_6 -X240_bit_5 X240_bit_4 X240_bit_3 X240_bit_2 -X240_bit_1 -X240_bit0 X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 X244_bit_6 -X244_bit_5 X244_bit_4 X244_bit_3 X244_bit_2 -X244_bit_1 -X244_bit0 X244_bit1 X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 -X245_bit_6 -X245_bit_5 X245_bit_4 X245_bit_3 -X245_bit_2 -X245_bit_1 X245_bit0 X245_bit1 X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 X246_bit_7 -X246_bit_6 X246_bit_5 X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 X247_bit_7 X247_bit_6 -X247_bit_5 X247_bit_4 X247_bit_3 X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 X248_bit_6 X248_bit_5 X248_bit_4 X248_bit_3 X248_bit_2 -X248_bit_1 X248_bit0 X248_bit1 X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 X249_bit_7 -X249_bit_6 X249_bit_5 X249_bit_4 X249_bit_3 X249_bit_2 X249_bit_1 -X249_bit0 X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 X250_bit_5 X250_bit_4 X250_bit_3 X250_bit_2 -X250_bit_1 X250_bit0 X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 -X251_bit_5 -X251_bit_4 -X251_bit_3 -X251_bit_2 -X251_bit_1 X251_bit0 X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 -X252_bit_6 -X252_bit_5 X252_bit_4 -X252_bit_3 X252_bit_2 -X252_bit_1 -X252_bit0 X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 -X253_bit_6 -X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 -X254_bit_6 -X254_bit_5 X254_bit_4 -X254_bit_3 X254_bit_2 -X254_bit_1 -X254_bit0 X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 X255_bit_6 -X255_bit_5 X255_bit_4 X255_bit_3 X255_bit_2 -X255_bit_1 -X255_bit0 X255_bit1 X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 Y9_bit0 Y10_bit0 -Y11_bit0 -Y12_bit0 Y13_bit0 Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 Y19_bit0 Y20_bit0 -Y21_bit0 Y22_bit0 Y23_bit0 -Y24_bit0 -Y25_bit0 Y26_bit0 -Y27_bit0 -Y28_bit0 Y29_bit0 Y30_bit0 Y31_bit0 Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 Y36_bit0 -Y37_bit0 Y38_bit0 Y39_bit0 Y40_bit0 -Y41_bit0 Y42_bit0 -Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 -Y51_bit0 Y52_bit0 Y53_bit0 Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 Y58_bit0 Y59_bit0 Y60_bit0 -Y61_bit0 -Y62_bit0 Y63_bit0 Y64_bit0 -Y65_bit0 -Y66_bit0 -Y67_bit0 -Y68_bit0 Y69_bit0 Y70_bit0 Y71_bit0 Y72_bit0 -Y73_bit0 -Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 Y79_bit0 -Y80_bit0 Y81_bit0 Y82_bit0 Y83_bit0 -Y84_bit0 Y85_bit0 -Y86_bit0 Y87_bit0 -Y88_bit0 Y89_bit0 -Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 Y95_bit0 -Y96_bit0 Y97_bit0 -Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 Y104_bit0 -Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 Y110_bit0 Y111_bit0 -Y112_bit0 -Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 Y118_bit0 Y119_bit0 -Y120_bit0 -Y121_bit0 Y122_bit0 -Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 -Y128_bit0 -Y129_bit0 -Y130_bit0 Y131_bit0 Y132_bit0 -Y133_bit0 -Y134_bit0 -Y135_bit0 Y136_bit0 Y137_bit0 Y138_bit0 -Y139_bit0 Y140_bit0 Y141_bit0 Y142_bit0 Y143_bit0 Y1#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.89 0.94 0.90 2/54 21210
Raw data (stat): 21210 (runsolver) R 21209 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541046655 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 2356 0 0 0 993 6 0 0 25 0 1 0 541046655 11952128 2281 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2918 2281 603 41 0 2877 0
vsize: 11672
[startup+20.0007 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 2778 0 0 0 1990 8 0 0 25 0 1 0 541046655 13651968 2703 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3333 2703 603 41 0 3292 0
vsize: 13332
[startup+30.0014 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 2997 0 0 0 2990 9 0 0 25 0 1 0 541046655 14458880 2922 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3530 2922 603 41 0 3489 0
vsize: 14120
[startup+40.0025 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 3211 0 0 0 3989 10 0 0 25 0 1 0 541046655 15532032 3136 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3792 3136 603 41 0 3751 0
vsize: 15168
[startup+50.0027 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 3577 0 0 0 4988 11 0 0 25 0 1 0 541046655 16879616 3502 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4121 3502 603 41 0 4080 0
vsize: 16484
[startup+60.0025 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 3941 0 0 0 5985 13 0 0 25 0 1 0 541046655 18358272 3866 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4482 3866 603 41 0 4441 0
vsize: 17928
[startup+70.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 4416 0 0 0 6984 15 0 0 25 0 1 0 541046655 20242432 4341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4942 4341 603 41 0 4901 0
vsize: 19768
[startup+80.0029 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 5077 0 0 0 7981 18 0 0 25 0 1 0 541046655 23199744 5002 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5664 5002 603 41 0 5623 0
vsize: 22656
[startup+90.0025 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 5473 0 0 0 8980 19 0 0 25 0 1 0 541046655 24817664 5398 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6059 5398 603 41 0 6018 0
vsize: 24236
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 5616 0 0 0 9979 20 0 0 25 0 1 0 541046655 25362432 5541 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6192 5541 603 41 0 6151 0
vsize: 24768
[startup+110.003 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 5998 0 0 0 10978 21 0 0 25 0 1 0 541046655 26972160 5923 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6585 5923 603 41 0 6544 0
vsize: 26340
[startup+120.004 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 11977 22 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+130.004 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 12977 23 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+140.004 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 13976 23 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+150.004 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 14976 24 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+160.004 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 15976 24 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+170.003 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 16975 25 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+180.004 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6210 0 0 0 17975 25 0 0 25 0 1 0 541046655 27783168 6135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6135 603 41 0 6742 0
vsize: 27132
[startup+190.005 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6211 0 0 0 18975 25 0 0 25 0 1 0 541046655 27783168 6136 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6783 6136 603 41 0 6742 0
vsize: 27132
[startup+200.004 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6211 0 0 0 19975 25 0 0 25 0 1 0 541046655 27783168 6136 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6783 6136 603 41 0 6742 0
vsize: 27132
[startup+210.004 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6211 0 0 0 20975 25 0 0 25 0 1 0 541046655 27783168 6136 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6783 6136 603 41 0 6742 0
vsize: 27132
[startup+220.004 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 6704 0 0 0 21974 27 0 0 25 0 1 0 541046655 29806592 6629 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7277 6629 603 41 0 7236 0
vsize: 29108
[startup+230.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7296 0 0 0 22972 29 0 0 25 0 1 0 541046655 32092160 7221 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7835 7221 603 41 0 7794 0
vsize: 31340
[startup+240.004 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7482 0 0 0 23972 29 0 0 25 0 1 0 541046655 32903168 7407 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7407 603 41 0 7992 0
vsize: 32132
[startup+250.004 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7482 0 0 0 24972 29 0 0 25 0 1 0 541046655 32903168 7407 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7407 603 41 0 7992 0
vsize: 32132
[startup+260.004 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7483 0 0 0 25972 29 0 0 25 0 1 0 541046655 32903168 7408 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7408 603 41 0 7992 0
vsize: 32132
[startup+270.004 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7483 0 0 0 26972 29 0 0 25 0 1 0 541046655 32903168 7408 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7408 603 41 0 7992 0
vsize: 32132
[startup+280.005 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7485 0 0 0 27972 29 0 0 25 0 1 0 541046655 32903168 7410 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7410 603 41 0 7992 0
vsize: 32132
[startup+290.005 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7487 0 0 0 28973 29 0 0 25 0 1 0 541046655 32903168 7412 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7412 603 41 0 7992 0
vsize: 32132
[startup+300.005 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7489 0 0 0 29973 29 0 0 25 0 1 0 541046655 32903168 7414 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7414 603 41 0 7992 0
vsize: 32132
[startup+310.006 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7489 0 0 0 30973 29 0 0 25 0 1 0 541046655 32903168 7414 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8033 7414 603 41 0 7992 0
vsize: 32132
[startup+320.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 7804 0 0 0 31972 30 0 0 25 0 1 0 541046655 34246656 7729 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8361 7729 603 41 0 8320 0
vsize: 33444
[startup+330.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 8173 0 0 0 32972 31 0 0 25 0 1 0 541046655 35737600 8098 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8725 8098 603 41 0 8684 0
vsize: 34900
[startup+340.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 8524 0 0 0 33971 31 0 0 25 0 1 0 541046655 37212160 8449 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9085 8449 603 41 0 9044 0
vsize: 36340
[startup+350.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 8914 0 0 0 34971 32 0 0 25 0 1 0 541046655 38838272 8839 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9482 8839 603 41 0 9441 0
vsize: 37928
[startup+360.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 9223 0 0 0 35970 33 0 0 25 0 1 0 541046655 40099840 9148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9790 9148 603 41 0 9749 0
vsize: 39160
[startup+370.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 9552 0 0 0 36970 34 0 0 25 0 1 0 541046655 41447424 9477 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10119 9477 603 41 0 10078 0
vsize: 40476
[startup+380.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 9871 0 0 0 37969 35 0 0 25 0 1 0 541046655 42811392 9796 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10452 9796 603 41 0 10411 0
vsize: 41808
[startup+390.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 10190 0 0 0 38968 36 0 0 25 0 1 0 541046655 44154880 10115 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10780 10115 603 41 0 10739 0
vsize: 43120
[startup+400.007 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 10295 0 0 0 39967 37 0 0 25 0 1 0 541046655 44560384 10220 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10879 10220 603 41 0 10838 0
vsize: 43516
[startup+410.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 10501 0 0 0 40967 37 0 0 25 0 1 0 541046655 45363200 10426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11075 10426 603 41 0 11034 0
vsize: 44300
[startup+420.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 10691 0 0 0 41966 38 0 0 25 0 1 0 541046655 46174208 10616 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11273 10616 603 41 0 11232 0
vsize: 45092
[startup+430.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 10813 0 0 0 42966 38 0 0 25 0 1 0 541046655 46714880 10738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11405 10738 603 41 0 11364 0
vsize: 45620
[startup+440.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11000 0 0 0 43966 38 0 0 25 0 1 0 541046655 47910912 10925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10925 603 41 0 11656 0
vsize: 46788
[startup+450.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 44966 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+460.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 45966 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+470.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 46966 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+480.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 47967 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+490.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 48967 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+500.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 49967 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+510.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 50967 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+520.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 51967 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+530.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 52968 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+540.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11002 0 0 0 53968 38 0 0 25 0 1 0 541046655 47910912 10927 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10927 603 41 0 11656 0
vsize: 46788
[startup+550.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 54968 38 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+560.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 55968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223668 134566145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+570.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 56967 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+580.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 57967 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+590.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 58967 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+600.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 59967 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+610.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 60968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+620.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 61968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+630.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 62968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+640.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 63968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+650.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 64968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+660.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 65968 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+670.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 66969 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+680.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 67969 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+690.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 68969 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+700.011 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 69969 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+710.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 70969 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+720.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11005 0 0 0 71970 39 0 0 25 0 1 0 541046655 47910912 10930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11697 10930 603 41 0 11656 0
vsize: 46788
[startup+730.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11097 0 0 0 72970 40 0 0 25 0 1 0 541046655 48328704 11022 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11799 11022 603 41 0 11758 0
vsize: 47196
[startup+740.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 73969 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+750.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 74969 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+760.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 75970 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+770.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 76970 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+780.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 77970 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 78970 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+800.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11262 0 0 0 79970 40 0 0 25 0 1 0 541046655 49000448 11187 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11963 11187 603 41 0 11922 0
vsize: 47852
[startup+810.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11665 0 0 0 80969 41 0 0 25 0 1 0 541046655 50532352 11507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11507 603 41 0 12296 0
vsize: 49348
[startup+820.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11670 0 0 0 81969 41 0 0 25 0 1 0 541046655 50532352 11512 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11512 603 41 0 12296 0
vsize: 49348
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11673 0 0 0 82970 41 0 0 25 0 1 0 541046655 50532352 11515 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11515 603 41 0 12296 0
vsize: 49348
[startup+840.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11673 0 0 0 83970 41 0 0 25 0 1 0 541046655 50532352 11515 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11515 603 41 0 12296 0
vsize: 49348
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11674 0 0 0 84970 41 0 0 25 0 1 0 541046655 50532352 11516 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11516 603 41 0 12296 0
vsize: 49348
[startup+860.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11674 0 0 0 85970 41 0 0 25 0 1 0 541046655 50532352 11516 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11516 603 41 0 12296 0
vsize: 49348
[startup+870.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11674 0 0 0 86970 41 0 0 25 0 1 0 541046655 50532352 11516 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12337 11516 603 41 0 12296 0
vsize: 49348
[startup+880.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 87971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+890.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 88971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+900.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 89971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223696 134565094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+910.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 90971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+920.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 91971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+930.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11706 0 0 0 92971 41 0 0 25 0 1 0 541046655 50692096 11548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11548 603 41 0 12335 0
vsize: 49504
[startup+940.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 93972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134561531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+950.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 94972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+960.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 95972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+970.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 96972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 97972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223680 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 98972 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223648 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 99973 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 100973 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 101973 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 102973 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 103973 41 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 104973 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 105973 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 106974 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 107974 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 108974 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11709 0 0 0 109974 42 0 0 25 0 1 0 541046655 50692096 11551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12376 11551 603 41 0 12335 0
vsize: 49504
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11860 0 0 0 110974 42 0 0 25 0 1 0 541046655 51228672 11702 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 11702 603 41 0 12466 0
vsize: 50028
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 11964 0 0 0 111974 42 0 0 25 0 1 0 541046655 51765248 11806 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12638 11806 603 41 0 12597 0
vsize: 50552
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 12085 0 0 0 112974 42 0 0 25 0 1 0 541046655 52166656 11927 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12736 11927 603 41 0 12695 0
vsize: 50944
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 12238 0 0 0 113973 43 0 0 25 0 1 0 541046655 52838400 12080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12900 12080 603 41 0 12859 0
vsize: 51600
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 12291 0 0 0 114974 43 0 0 25 0 1 0 541046655 53108736 12133 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12966 12133 603 41 0 12925 0
vsize: 51864
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 12726 0 0 0 115973 44 0 0 25 0 1 0 541046655 54870016 12568 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13396 12568 603 41 0 13355 0
vsize: 53584
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 12865 0 0 0 116973 45 0 0 25 0 1 0 541046655 55410688 12707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13528 12707 603 41 0 13487 0
vsize: 54112
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 13051 0 0 0 117972 45 0 0 25 0 1 0 541046655 56078336 12893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13691 12893 603 41 0 13650 0
vsize: 54764
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 13347 0 0 0 118971 46 0 0 25 0 1 0 541046655 57290752 13189 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13987 13189 603 41 0 13946 0
vsize: 55948
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21210
Raw data (stat): 21210 (minisat+) R 21209 22612 22611 0 -1 0 13438 0 0 0 119971 46 0 0 25 0 1 0 541046655 57511936 13255 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14041 13255 603 41 0 14000 0
vsize: 56164
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 21210
Raw data (stat): 21210 (minisat+) Z 21209 22612 22611 0 -1 12 13441 0 0 0 119972 49 0 0 25 0 1 0 541046655 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.73
CPU system time (s): 0.494924
CPU usage (%): 100.014
Max. virtual memory (Kb): 56164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####