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/milp/normalized-mps-v2-13-7-ran14x18_1.opb
MD5SUM	27cc6bcebfcedf07c5cf3ac138a419c6
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	913429
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
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	1421968313
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	1421968313
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.03
Number of variables	5292
Total number of constraints	536
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	252
Number of constraints which are nor clauses,nor cardinality constraints	284
Minimum length of a constraint	1
Maximum length of a constraint	360
Trace number 14522

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        638440 kB
Buffers:         34220 kB
Cached:         330824 kB
SwapCached:        388 kB
Active:         116332 kB
Inactive:       251220 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        638188 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6224 kB
Slab:            22944 kB
Committed_AS:    63804 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 00:30:19 (client local time) WITH STATUS 10 IN 1200.34 SECONDS
stats: 19809 7 1200.34 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 316 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 314]---> Adder-cost: 386   maxlim: 47470   bits: 16/16
c ---[ 312]---> Adder-cost: 386   maxlim: 47726   bits: 16/16
c ---[ 310]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 308]---> Adder-cost: 388   maxlim: 58222   bits: 16/16
c ---[ 306]---> Adder-cost: 386   maxlim: 47342   bits: 16/16
c ---[ 304]---> Adder-cost: 386   maxlim: 46830   bits: 16/16
c ---[ 302]---> Adder-cost: 386   maxlim: 47086   bits: 16/16
c ---[ 300]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 298]---> Adder-cost: 386   maxlim: 46702   bits: 16/16
c ---[ 296]---> Adder-cost: 386   maxlim: 46958   bits: 16/16
c ---[ 294]---> Adder-cost: 372   maxlim: 32494   bits: 16/15
c ---[ 292]---> Adder-cost: 386   maxlim: 48110   bits: 16/16
c ---[ 290]---> Adder-cost: 386   maxlim: 47982   bits: 16/16
c ---[ 288]---> Adder-cost: 388   maxlim: 57582   bits: 16/16
c ---[ 286]---> Adder-cost: 260   maxlim: 13554   bits: 14/14
c ---[ 284]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 282]---> Adder-cost: 260   maxlim: 13426   bits: 14/14
c ---[ 280]---> Adder-cost: 310   maxlim: 50930   bits: 16/16
c ---[ 278]---> Adder-cost: 286   maxlim: 26866   bits: 15/15
c ---[ 276]---> Adder-cost: 310   maxlim: 50418   bits: 16/16
c ---[ 274]---> Adder-cost: 312   maxlim: 57202   bits: 16/16
c ---[ 272]---> Adder-cost: 312   maxlim: 55666   bits: 16/16
c ---[ 270]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 268]---> Adder-cost: 286   maxlim: 27634   bits: 15/15
c ---[ 266]---> Adder-cost: 310   maxlim: 50546   bits: 16/16
c ---[ 264]---> Adder-cost: 286   maxlim: 27250   bits: 15/15
c ---[ 262]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 260]---> Adder-cost: 260   maxlim: 13810   bits: 14/14
c ---[ 258]---> Adder-cost: 312   maxlim: 56946   bits: 16/16
c ---[ 256]---> Adder-cost: 286   maxlim: 26994   bits: 15/15
c ---[ 254]---> Adder-cost: 310   maxlim: 50674   bits: 16/16
c ---[ 252]---> Adder-cost: 286   maxlim: 27506   bits: 15/15
c ---[ 251]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 249]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 248]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 247]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 246]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 245]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 244]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 243]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 242]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 240]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 237]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 236]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 235]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 234]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 232]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 231]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 227]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 226]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 225]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 224]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 223]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 221]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 219]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 218]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 217]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 216]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 215]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 214]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 212]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 211]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 210]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 209]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 205]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 204]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 203]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 202]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 200]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 199]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 198]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 197]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 196]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 195]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 194]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 193]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 192]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 188]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 187]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 186]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 185]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 184]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 183]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 181]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 180]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 179]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 177]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 175]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 173]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 172]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 170]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 169]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 168]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 167]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 165]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 164]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 163]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 162]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 161]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 160]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 159]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 157]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 156]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 153]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 152]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 150]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 149]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 148]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 147]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 145]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 144]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 143]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 141]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 138]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 137]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 136]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 134]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 132]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 131]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 130]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 127]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 124]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 123]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 122]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 119]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 118]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 115]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 114]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 113]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 112]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 111]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 110]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 109]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 107]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 106]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 105]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 104]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 103]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 102]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 100]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  98]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  97]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  95]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  93]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  92]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  91]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  89]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  87]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  85]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  83]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  82]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  80]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  77]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  76]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  75]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  71]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  70]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  69]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  66]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  62]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  61]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  54]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  52]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  50]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  45]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  41]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  35]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  34]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  30]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  26]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  25]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  20]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  19]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  14]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  13]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   7]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   82180   302580 |   27393       0        0     nan |  0.000 % |
c |       100 |   82180   302580 |   30132     100      285     2.9 | 28.708 % |
c |       250 |   82157   302507 |   33145     248     1010     4.1 | 28.727 % |
c |       475 |   82124   302396 |   36460     471     2004     4.3 | 28.756 % |
c |       814 |   81989   301943 |   40106     786     3130     4.0 | 28.875 % |
c |      1320 |   81789   301271 |   44116    1266     5034     4.0 | 29.047 % |
c |      2079 |   81696   300944 |   48528    2009     8367     4.2 | 29.119 % |
c |      3219 |   81457   300143 |   53381    3111    14076     4.5 | 29.325 % |
c |      4929 |   81058   298770 |   58719    4760    24352     5.1 | 29.669 % |
c |      7491 |   80586   297198 |   64591    7256    36509     5.0 | 30.094 % |
c |     11335 |   80065   295433 |   71050   11028    55499     5.0 | 30.543 % |
c |     17102 |   79700   294188 |   78155   16753    87374     5.2 | 30.864 % |
c |     25751 |   79148   292330 |   85970   25329   135531     5.4 | 31.346 % |
c |     38725 |   78766   291042 |   94568   38251   220588     5.8 | 31.672 % |
c |     58186 |   78400   289828 |  104024   57650   392235     6.8 | 32.001 % |
c |     87378 |   78223   289217 |  114427   86816  1006589    11.6 | 32.154 % |
c ==============================================================================
c [1mFound solution: 5357649[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10447   maxlim: 3631976   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    109069 |  151049   549410 |   50349  108471  1434164    13.2 | 32.154 % |
c |    109169 |  151049   549410 |   55383   26915   352305    13.1 | 21.605 % |
c |    109319 |  151049   549410 |   60922   27065   353038    13.0 | 21.605 % |
c |    109544 |  151049   549410 |   67014   27290   354054    13.0 | 21.605 % |
c |    109881 |  151040   549381 |   73715   27626   355838    12.9 | 21.611 % |
c |    110387 |  151040   549381 |   81087   28132   359704    12.8 | 21.611 % |
c |    111146 |  151040   549381 |   89196   28891   365050    12.6 | 21.611 % |
c |    112285 |  151040   549381 |   98115   30030   372474    12.4 | 21.611 % |
c |    113994 |  151040   549381 |  107927   31739   388860    12.3 | 21.611 % |
c |    116556 |  151024   549329 |  118720   34299   408820    11.9 | 21.621 % |
c |    120400 |  151024   549329 |  130592   38143   495782    13.0 | 21.621 % |
c |    126166 |  151017   549306 |  143651   43908   548779    12.5 | 21.624 % |
c |    134815 |  150981   549190 |  158016   52552   641400    12.2 | 21.649 % |
c |    147789 |  150981   549190 |  173818   65526  1017071    15.5 | 21.649 % |
c |    167250 |  150937   549040 |  191200   84981  1270324    14.9 | 21.672 % |
c |    196446 |  150889   548882 |  210320  114171  1930302    16.9 | 21.697 % |
c ==============================================================================
c [1mFound solution: 4724138[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4265487   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    235126 |  150852   548810 |   50284  152843  3565495    23.3 | 21.697 % |
c |    235226 |  150852   548810 |   55312   31184   656795    21.1 | 21.746 % |
c |    235376 |  150852   548810 |   60843   31334   657562    21.0 | 21.746 % |
c |    235602 |  150852   548810 |   66928   31560   658598    20.9 | 21.746 % |
c |    235940 |  150852   548810 |   73620   31898   660313    20.7 | 21.746 % |
c |    236446 |  150852   548810 |   80982   32404   662609    20.4 | 21.746 % |
c |    237205 |  150852   548810 |   89081   33163   666067    20.1 | 21.746 % |
c |    238344 |  150852   548810 |   97989   34302   672065    19.6 | 21.746 % |
c |    240053 |  150845   548787 |  107788   36009   686918    19.1 | 21.749 % |
c |    242615 |  150845   548787 |  118567   38571   715642    18.6 | 21.749 % |
c |    246459 |  150845   548787 |  130423   42415   750437    17.7 | 21.749 % |
c |    252225 |  150845   548787 |  143466   48181   871182    18.1 | 21.749 % |
c |    260874 |  150822   548708 |  157812   56827   979011    17.2 | 21.762 % |
c |    273848 |  150822   548708 |  173594   69801  1141578    16.4 | 21.762 % |
c |    293309 |  150792   548606 |  190953   89257  1399147    15.7 | 21.778 % |
c |    322501 |  150767   548525 |  210048  118446  2055173    17.4 | 21.794 % |
c |    366290 |  150731   548405 |  231053  162228  5464765    33.7 | 21.813 % |
c ==============================================================================
c [1mFound solution: 4074377[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4915248   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    416416 |  150731   548477 |   50243  212350  7573616    35.7 | 21.813 % |
c |    416516 |  150731   548477 |   55267   34801   323417     9.3 | 21.833 % |
c |    416667 |  150731   548477 |   60794   34952   324135     9.3 | 21.833 % |
c |    416892 |  150731   548477 |   66873   35177   325357     9.2 | 21.833 % |
c |    417229 |  150731   548477 |   73560   35514   327031     9.2 | 21.833 % |
c |    417735 |  150731   548477 |   80916   36020   329905     9.2 | 21.833 % |
c |    418494 |  150731   548477 |   89008   36779   334064     9.1 | 21.833 % |
c |    419633 |  150731   548477 |   97909   37918   343241     9.1 | 21.833 % |
c |    421342 |  150731   548477 |  107700   39627   356390     9.0 | 21.833 % |
c |    423904 |  150731   548477 |  118470   42189   381689     9.0 | 21.833 % |
c |    427748 |  150731   548477 |  130317   46033   435489     9.5 | 21.833 % |
c |    433514 |  150731   548477 |  143349   51799   494298     9.5 | 21.833 % |
c |    442163 |  150731   548477 |  157684   60448   606359    10.0 | 21.833 % |
c |    455139 |  150699   548367 |  173452   73420   798459    10.9 | 21.849 % |
c |    474600 |  150699   548367 |  190797   92881  1477174    15.9 | 21.849 % |
c |    503792 |  150683   548315 |  209877  122069  2363539    19.4 | 21.859 % |
c |    547581 |  150683   548315 |  230865  165858  5563340    33.5 | 21.859 % |
c ==============================================================================
c [1mFound solution: 3949715[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5039910   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    556369 |  150702   548517 |   50234  174646  5928504    33.9 | 21.859 % |
c |    556469 |  150702   548517 |   55257   33456   616541    18.4 | 21.885 % |
c |    556619 |  150702   548517 |   60783   33606   617157    18.4 | 21.885 % |
c |    556844 |  150702   548517 |   66861   33831   618068    18.3 | 21.885 % |
c |    557182 |  150702   548517 |   73547   34169   619510    18.1 | 21.885 % |
c |    557688 |  150702   548517 |   80902   34675   622254    17.9 | 21.885 % |
c |    558447 |  150702   548517 |   88992   35434   627473    17.7 | 21.885 % |
c |    559586 |  150702   548517 |   97891   36573   634065    17.3 | 21.885 % |
c |    561294 |  150702   548517 |  107681   38281   646259    16.9 | 21.885 % |
c |    563857 |  150702   548517 |  118449   40844   678200    16.6 | 21.885 % |
c |    567701 |  150702   548517 |  130294   44688   718335    16.1 | 21.885 % |
c |    573468 |  150702   548517 |  143323   50455   781013    15.5 | 21.885 % |
c |    582117 |  150702   548517 |  157655   59104   955724    16.2 | 21.885 % |
c |    595091 |  150702   548517 |  173421   72078  1256918    17.4 | 21.885 % |
c |    614552 |  150693   548486 |  190763   91533  1652974    18.1 | 21.888 % |
c |    643744 |  150693   548486 |  209839  120725  3115601    25.8 | 21.888 % |
c ==============================================================================
c [1mFound solution: 3478754[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 5510871   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    663613 |  150701   548614 |   50233  140590  3531848    25.1 | 21.888 % |
c |    663713 |  150701   548614 |   55256   33915   278826     8.2 | 21.911 % |
c |    663863 |  150701   548614 |   60781   34065   279578     8.2 | 21.911 % |
c |    664088 |  150701   548614 |   66860   34290   280803     8.2 | 21.911 % |
c |    664425 |  150701   548614 |   73546   34627   282558     8.2 | 21.911 % |
c |    664932 |  150701   548614 |   80900   35134   285050     8.1 | 21.911 % |
c |    665691 |  150701   548614 |   88990   35893   289109     8.1 | 21.911 % |
c |    666830 |  150701   548614 |   97889   37032   295958     8.0 | 21.911 % |
c |    668538 |  150701   548614 |  107678   38740   307250     7.9 | 21.911 % |
c |    671100 |  150701   548614 |  118446   41302   327641     7.9 | 21.911 % |
c |    674944 |  150701   548614 |  130291   45146   372754     8.3 | 21.911 % |
c |    680710 |  150701   548614 |  143320   50912   825651    16.2 | 21.911 % |
c |    689359 |  150701   548614 |  157652   59561   943480    15.8 | 21.911 % |
c |    702333 |  150701   548614 |  173417   72535  1096636    15.1 | 21.911 % |
c |    721794 |  150701   548614 |  190759   91996  2100077    22.8 | 21.911 % |
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 Y0_bit0 Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 -Y9_bit0 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 Y10_bit0 -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 Y11_bit0 -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 Y12_bit0 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 -Y13_bit0 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 Y14_bit0 Y15_bit0 -Y16_bit0 -Y17_bit0 -Y18_bit0 Y19_bit0 -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 Y20_bit0 -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 Y21_bit0 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 -Y22_bit0 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 Y23_bit0 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 -Y24_bit0 -Y25_bit0 -Y26_bit0 -Y27_bit0 -Y28_bit0 Y29_bit0 -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 Y30_bit0 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 -Y31_bit0 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 -Y32_bit0 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 Y33_bit0 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 Y34_bit0 Y35_bit0 Y36_bit0 -Y37_bit0 -Y38_bit0 Y39_bit0 -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 Y40_bit0 -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 -Y41_bit0 -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 Y42_bit0 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 Y43_bit0 -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 Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 -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 Y50_bit0 -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 Y51_bit0 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 Y52_bit0 -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 -Y53_bit0 -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 -Y54_bit0 -Y55_bit0 Y56_bit0 Y57_bit0 Y58_bit0 Y59_bit0 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 -Y60_bit0 -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 Y61_bit0 -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 Y62_bit0 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 -Y63_bit0 -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 Y64_bit0 Y65_bit0 -Y66_bit0 -Y67_bit0 -Y68_bit0 Y69_bit0 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 -Y70_bit0 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 Y71_bit0 -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 Y72_bit0 -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 -Y73_bit0 -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 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 -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 Y100_bit0 Y101_bit0 Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 Y110_bit0 -Y111_bit0 -Y112_bit0 Y113_bit0 -Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 Y118_bit0 -Y119_bit0 -Y120_bit0 Y121_bit0 -Y122_bit0 Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 -Y127_bit0 -Y128_bit0 -Y129_bit0 Y130_bit0 Y131_bit0 Y132_bit0 Y133_bit0 Y134_bit0 -Y135_bit0 -Y136_bit0 -Y137_bit0 Y138_bit0 Y139_bit0 -Y140_bit0 Y141_bit0 Y142_bit0 Y143_bit0 Y144_bit0 Y145_bit0 -Y146_bit0 Y147_bit0 Y148_bit0 Y149_bit0 -Y150_bit0 Y151_bit0 -Y152_bit0 -Y153_bit0 -Y154_bit0 Y155_bit0 Y156_bit0 Y157_bit0 Y158_bit0 Y159_bit0 -Y160_bit0 Y161_bit0 -Y162_bit0 Y163_bit0 Y164_bit0 -Y165_bit0 -Y166_bit0 Y167_bit0 Y168_bit0 Y169_bit0 -Y170_bit0 Y171_bit0 Y172_bit0 Y173_bit0 Y174_bit0 Y175_bit0 -Y176_bit0 Y177_bit0 -Y178_bit0 -Y179_bit0 Y180_bit0 Y181_bit0 Y182_bit0 Y183_bit0 Y184_bit0 Y185_bit0 -Y186_bit0 -Y187_bit0 Y188_bit0 -Y189_bit0 Y190_bit0 Y191_bit0 Y192_bit0 Y193_bit0 Y194_bit0 -Y195_bit0 Y196_bit0 -Y197_bit0 Y198_bit0 -Y199_bit0 Y200_bit0 Y201_bit0 Y202_bit0 -Y203_bit0 -Y204_bit0 Y205_bit0 -Y206_bit0 -Y207_bit0 Y208_bit0 -Y209_bit0 Y210_bit0 Y211_bit0 Y212_bit0 Y213_bit0 Y214_bit0 Y215_bit0 Y216_bit0 Y217_bit0 Y218_bit0 Y219_bit0 Y220_bit0 Y221_bit0 Y222_bit0 Y223_bit0 Y224_bit0 Y225_bit0 Y226_bit0 -Y227_bit0 -Y228_bit0 -Y229#### 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.93 0.98 0.94 2/55 13813
Raw data (stat): 13813 (runsolver) R 13812 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540642848 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.0006 s]
Raw data (loadavg): 0.94 0.98 0.94 2/55 13813
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2434 0 0 0 993 6 0 0 25 0 1 0 540642848 12562432 2359 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3067 2359 603 41 0 3026 0
vsize: 12268
[startup+20.0019 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 13813
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2508 0 0 0 1992 6 0 0 25 0 1 0 540642848 12963840 2433 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3165 2433 603 41 0 3124 0
vsize: 12660
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2589 0 0 0 2991 7 0 0 25 0 1 0 540642848 13303808 2514 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3248 2514 603 41 0 3207 0
vsize: 12992
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2661 0 0 0 3991 8 0 0 25 0 1 0 540642848 13570048 2586 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3313 2586 603 41 0 3272 0
vsize: 13252
[startup+50.0036 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2746 0 0 0 4991 8 0 0 25 0 1 0 540642848 13840384 2671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3379 2671 603 41 0 3338 0
vsize: 13516
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2836 0 0 0 5990 9 0 0 25 0 1 0 540642848 14245888 2761 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3478 2761 603 41 0 3437 0
vsize: 13912
[startup+70.0045 s]
Raw data (loadavg): 0.97 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 2929 0 0 0 6989 10 0 0 25 0 1 0 540642848 14778368 2854 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3608 2854 603 41 0 3567 0
vsize: 14432
[startup+80.0054 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3041 0 0 0 7989 10 0 0 25 0 1 0 540642848 15183872 2966 4294967295 134512640 134672761 3221224544 3221223696 134565083 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3707 2966 603 41 0 3666 0
vsize: 14828
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3169 0 0 0 8988 11 0 0 25 0 1 0 540642848 15724544 3094 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3839 3094 603 41 0 3798 0
vsize: 15356
[startup+100.005 s]
Raw data (loadavg): 0.98 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3299 0 0 0 9988 11 0 0 25 0 1 0 540642848 16125952 3224 4294967295 134512640 134672761 3221224544 3221223696 134565103 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3937 3224 603 41 0 3896 0
vsize: 15748
[startup+110.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3443 0 0 0 10987 12 0 0 25 0 1 0 540642848 16797696 3368 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4101 3368 603 41 0 4060 0
vsize: 16404
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3600 0 0 0 11986 13 0 0 25 0 1 0 540642848 17596416 3525 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4296 3525 603 41 0 4255 0
vsize: 17184
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 3814 0 0 0 12986 14 0 0 25 0 1 0 540642848 18403328 3739 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4493 3739 603 41 0 4452 0
vsize: 17972
[startup+140.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 4350 0 0 0 13984 16 0 0 25 0 1 0 540642848 20561920 4275 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5020 4275 603 41 0 4979 0
vsize: 20080
[startup+150.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 4528 0 0 0 14984 16 0 0 25 0 1 0 540642848 21237760 4453 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5185 4453 603 41 0 5144 0
vsize: 20740
[startup+160.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 4774 0 0 0 15983 17 0 0 25 0 1 0 540642848 22315008 4699 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5448 4699 603 41 0 5407 0
vsize: 21792
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6165 0 0 0 16980 20 0 0 25 0 1 0 540642848 27226112 6001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6001 603 41 0 6606 0
vsize: 26588
[startup+180.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6168 0 0 0 17980 21 0 0 25 0 1 0 540642848 27226112 6004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6004 603 41 0 6606 0
vsize: 26588
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6170 0 0 0 18979 21 0 0 25 0 1 0 540642848 27226112 6006 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6006 603 41 0 6606 0
vsize: 26588
[startup+200.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6171 0 0 0 19979 21 0 0 25 0 1 0 540642848 27226112 6007 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6007 603 41 0 6606 0
vsize: 26588
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6171 0 0 0 20979 22 0 0 25 0 1 0 540642848 27226112 6007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6007 603 41 0 6606 0
vsize: 26588
[startup+220.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6173 0 0 0 21979 22 0 0 25 0 1 0 540642848 27226112 6009 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6009 603 41 0 6606 0
vsize: 26588
[startup+230.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6174 0 0 0 22978 22 0 0 25 0 1 0 540642848 27226112 6010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6010 603 41 0 6606 0
vsize: 26588
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6174 0 0 0 23978 23 0 0 25 0 1 0 540642848 27226112 6010 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6010 603 41 0 6606 0
vsize: 26588
[startup+250.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6174 0 0 0 24978 23 0 0 25 0 1 0 540642848 27226112 6010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6647 6010 603 41 0 6606 0
vsize: 26588
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6174 0 0 0 25978 23 0 0 25 0 1 0 540642848 27226112 6010 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6647 6010 603 41 0 6606 0
vsize: 26588
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6174 0 0 0 26978 23 0 0 25 0 1 0 540642848 27226112 6010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6647 6010 603 41 0 6606 0
vsize: 26588
[startup+280.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6246 0 0 0 27978 23 0 0 25 0 1 0 540642848 27496448 6082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6713 6082 603 41 0 6672 0
vsize: 26852
[startup+290.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6374 0 0 0 28978 23 0 0 25 0 1 0 540642848 28037120 6210 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 6210 603 41 0 6804 0
vsize: 27380
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6471 0 0 0 29978 24 0 0 25 0 1 0 540642848 28442624 6307 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6944 6307 603 41 0 6903 0
vsize: 27776
[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 6671 0 0 0 30978 24 0 0 25 0 1 0 540642848 29249536 6507 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7141 6507 603 41 0 7100 0
vsize: 28564
[startup+320.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13815
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 7057 0 0 0 31977 26 0 0 25 0 1 0 540642848 30736384 6893 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7504 6893 603 41 0 7463 0
vsize: 30016
[startup+330.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 7162 0 0 0 32977 26 0 0 25 0 1 0 540642848 31141888 6998 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7603 6998 603 41 0 7562 0
vsize: 30412
[startup+340.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 7364 0 0 0 33976 27 0 0 25 0 1 0 540642848 31948800 7200 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7800 7200 603 41 0 7759 0
vsize: 31200
[startup+350.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 7519 0 0 0 34976 27 0 0 25 0 1 0 540642848 33148928 7355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8093 7355 603 41 0 8052 0
vsize: 32372
[startup+360.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 8261 0 0 0 35974 29 0 0 25 0 1 0 540642848 36118528 8097 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8818 8097 603 41 0 8777 0
vsize: 35272
[startup+370.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 8832 0 0 0 36973 30 0 0 25 0 1 0 540642848 38539264 8668 4294967295 134512640 134672761 3221224544 3221223712 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9409 8668 603 41 0 9368 0
vsize: 37636
[startup+380.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 8979 0 0 0 37973 31 0 0 25 0 1 0 540642848 39075840 8815 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9540 8815 603 41 0 9499 0
vsize: 38160
[startup+390.022 s]
Raw data (loadavg): 1.07 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 38972 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+400.023 s]
Raw data (loadavg): 1.06 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 39972 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+410.023 s]
Raw data (loadavg): 1.05 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 40972 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+420.024 s]
Raw data (loadavg): 1.04 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 41973 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+430.024 s]
Raw data (loadavg): 1.04 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 42973 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+440.024 s]
Raw data (loadavg): 1.03 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 43973 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+450.024 s]
Raw data (loadavg): 1.03 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 44973 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+460.127 s]
Raw data (loadavg): 1.02 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 45983 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+470.128 s]
Raw data (loadavg): 1.02 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 46984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+480.128 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 47984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+490.127 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 48984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+500.128 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 49984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+510.128 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 50984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134564689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+520.129 s]
Raw data (loadavg): 1.01 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 51984 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+530.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 52985 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+540.129 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 53985 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+550.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 54985 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+560.13 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 55985 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223712 134560979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+570.136 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9100 0 0 0 56986 32 0 0 25 0 1 0 540642848 39489536 8931 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9641 8931 603 41 0 9600 0
vsize: 38564
[startup+580.137 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9596 0 0 0 57985 33 0 0 25 0 1 0 540642848 41644032 9427 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10167 9427 603 41 0 10126 0
vsize: 40668
[startup+590.137 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 9741 0 0 0 58985 33 0 0 25 0 1 0 540642848 42184704 9572 4294967295 134512640 134672761 3221224544 3221223700 134565154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10299 9572 603 41 0 10258 0
vsize: 41196
[startup+600.138 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 10335 0 0 0 59984 34 0 0 25 0 1 0 540642848 44601344 10166 4294967295 134512640 134672761 3221224544 3221223648 134560226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10889 10166 603 41 0 10848 0
vsize: 43556
[startup+610.138 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 11122 0 0 0 60982 36 0 0 25 0 1 0 540642848 47824896 10953 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11676 10953 603 41 0 11635 0
vsize: 46704
[startup+620.139 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13817
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 11359 0 0 0 61982 37 0 0 25 0 1 0 540642848 48766976 11190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11906 11190 603 41 0 11865 0
vsize: 47624
[startup+630.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 11767 0 0 0 62981 38 0 0 25 0 1 0 540642848 50384896 11598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12301 11598 603 41 0 12260 0
vsize: 49204
[startup+640.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 12398 0 0 0 63979 40 0 0 25 0 1 0 540642848 52953088 12229 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12928 12229 603 41 0 12887 0
vsize: 51712
[startup+650.141 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 12521 0 0 0 64979 40 0 0 25 0 1 0 540642848 53493760 12352 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13060 12352 603 41 0 13019 0
vsize: 52240
[startup+660.14 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13152 0 0 0 65977 42 0 0 25 0 1 0 540642848 56045568 12983 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13683 12983 603 41 0 13642 0
vsize: 54732
[startup+670.141 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13391 0 0 0 66977 43 0 0 25 0 1 0 540642848 56983552 13222 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13912 13222 603 41 0 13871 0
vsize: 55648
[startup+680.141 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13550 0 0 0 67976 43 0 0 25 0 1 0 540642848 57655296 13381 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14076 13381 603 41 0 14035 0
vsize: 56304
[startup+690.141 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13743 0 0 0 68976 44 0 0 25 0 1 0 540642848 58327040 13574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14240 13574 603 41 0 14199 0
vsize: 56960
[startup+700.143 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 69976 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223808 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+710.143 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 70976 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+720.144 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 71976 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+730.144 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 72977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+740.144 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 73977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+750.145 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 74977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+760.145 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 75977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+770.147 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 76977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+780.146 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 77977 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+790.147 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 78978 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+800.147 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 79978 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+810.148 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 80978 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+820.15 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 81978 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+830.15 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 82978 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+840.15 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 83979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+850.15 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 84979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+860.15 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 85979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+870.151 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 86979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+880.151 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 87979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+890.151 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 88979 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+900.152 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13908 0 0 0 89980 44 0 0 25 0 1 0 540642848 58826752 13709 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13709 603 41 0 14321 0
vsize: 57448
[startup+910.152 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 90980 44 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223680 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+920.154 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13819
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 91980 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+930.154 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 92980 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+940.155 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 93980 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223780 134564428 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+950.156 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 94980 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+960.156 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 95980 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+970.157 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 96981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+980.157 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 97981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223744 134557915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+990.157 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 98981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1000.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 99981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1010.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 100981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1020.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 101982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1030.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 102981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1040.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 103981 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1050.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 104982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1060.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 105982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1070.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 106982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1080.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 107982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1090.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 108982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1100.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 109982 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1110.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 110983 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1120.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 111983 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1130.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 112983 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1140.16 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 113983 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1150.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 114983 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1160.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 115984 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1170.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 116984 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1180.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 117984 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223712 134561403 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1190.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 118984 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
[startup+1200.17 s]
Raw data (loadavg): 1.00 1.00 0.94 2/55 13821
Raw data (stat): 13813 (minisat+) R 13812 20024 20023 0 -1 0 13911 0 0 0 119984 45 0 0 25 0 1 0 540642848 58826752 13712 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14362 13712 603 41 0 14321 0
vsize: 57448
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.00 1.00 0.94 1/55 13821
Raw data (stat): 13813 (minisat+) Z 13812 20024 20023 0 -1 12 13914 0 0 0 119985 47 0 0 25 0 1 0 540642848 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.21
CPU time (s): 1200.34
CPU user time (s): 1199.86
CPU system time (s): 0.479927
CPU usage (%): 100.01
Max. virtual memory (Kb): 57448
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####