PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran16x16.opb
MD5SUM	9ccd6fd38eec7ec6eedca3a615a280ba
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1042560
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1526874453
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	1526874453
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	1175.06
Number of variables	5376
Total number of constraints	288
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	288
Minimum length of a constraint	21
Maximum length of a constraint	320
Trace number 17636

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        695944 kB
Buffers:         27320 kB
Cached:         289084 kB
SwapCached:          0 kB
Active:          64228 kB
Inactive:       255096 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        695692 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13784 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:22:20 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 19315 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 320 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 318]---> Adder-cost: 332   maxlim: 41712   bits: 16/16
c ---[ 316]---> Adder-cost: 332   maxlim: 41456   bits: 16/16
c ---[ 314]---> Adder-cost: 332   maxlim: 42096   bits: 16/16
c ---[ 312]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 310]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 308]---> Adder-cost: 316   maxlim: 24432   bits: 15/15
c ---[ 306]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 304]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 302]---> Adder-cost: 316   maxlim: 24816   bits: 15/15
c ---[ 300]---> Adder-cost: 268   maxlim: 7280   bits: 13/13
c ---[ 298]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 296]---> Adder-cost: 336   maxlim: 49904   bits: 16/16
c ---[ 294]---> Adder-cost: 316   maxlim: 24944   bits: 15/15
c ---[ 292]---> Adder-cost: 332   maxlim: 42352   bits: 16/16
c ---[ 290]---> Adder-cost: 316   maxlim: 24176   bits: 15/15
c ---[ 288]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 286]---> Adder-cost: 328   maxlim: 27760   bits: 15/15
c ---[ 284]---> Adder-cost: 344   maxlim: 44528   bits: 16/16
c ---[ 282]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 280]---> Adder-cost: 350   maxlim: 52208   bits: 16/16
c ---[ 278]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 276]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 274]---> Adder-cost: 344   maxlim: 43760   bits: 16/16
c ---[ 272]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 270]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 268]---> Adder-cost: 350   maxlim: 53616   bits: 16/16
c ---[ 266]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 264]---> Adder-cost: 344   maxlim: 44784   bits: 16/16
c ---[ 262]---> Adder-cost: 350   maxlim: 54640   bits: 16/16
c ---[ 260]---> Adder-cost: 328   maxlim: 28144   bits: 15/15
c ---[ 258]---> Adder-cost: 328   maxlim: 28016   bits: 15/15
c ---[ 256]---> Adder-cost: 344   maxlim: 45552   bits: 16/16
c ---[ 255]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 254]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 253]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 252]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 251]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 250]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 249]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 248]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 247]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 246]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 245]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 244]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 243]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 242]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 241]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 240]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 239]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 237]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 236]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 235]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 234]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 233]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 232]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 231]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 230]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 228]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 227]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 226]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 225]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 224]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 223]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 222]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 221]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 219]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 218]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 217]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 216]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 215]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 214]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 213]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 212]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 211]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 210]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 209]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 208]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 207]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 206]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 204]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 203]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 202]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 201]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 200]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 199]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 198]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 197]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 196]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 195]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 193]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 192]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 191]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 190]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 189]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 188]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 187]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 186]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 185]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 184]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 183]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 182]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 181]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 180]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 179]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 177]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 176]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 175]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 174]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 173]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 172]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 171]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 170]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 169]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 167]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 166]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 165]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 164]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 163]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 162]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 161]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 160]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 159]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 158]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 157]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 156]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 154]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 153]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 152]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 150]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 148]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 147]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 146]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 143]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 142]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 141]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 140]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 138]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 137]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 136]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 135]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 134]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 131]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 130]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 129]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 128]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 127]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 123]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 121]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 120]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 119]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 118]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 114]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 112]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 111]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 110]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 109]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 107]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 106]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 104]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 103]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 102]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 101]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 100]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  99]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  98]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  97]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  96]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  95]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  94]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  92]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  89]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  88]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  86]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  85]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  83]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  82]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  80]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  79]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  78]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  76]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  75]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  74]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  73]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  72]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  70]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  69]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  66]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  65]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  64]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  63]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  61]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  59]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  58]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  57]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  56]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  55]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  54]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  53]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  52]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  51]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  50]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  49]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  48]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  47]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  46]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  45]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  44]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  43]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  42]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  40]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  39]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  38]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  36]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  35]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  34]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  33]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  32]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  30]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  27]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  26]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  25]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  23]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  21]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  18]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  17]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  16]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  14]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  13]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  10]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   9]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   8]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[   7]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   5]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   3]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 2   maxlim: 510   bits: 10/9
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 |   77358   284117 |   25786       0        0     nan |  0.000 % |
c |       100 |   77358   284117 |   28364     100      287     2.9 | 30.132 % |
c |       251 |   77358   284117 |   31201     251     1128     4.5 | 30.132 % |
c |       478 |   77350   284091 |   34321     477     2120     4.4 | 30.137 % |
c |       815 |   77306   283933 |   37753     809     3746     4.6 | 30.171 % |
c |      1322 |   77234   283695 |   41528    1302     9327     7.2 | 30.236 % |
c |      2081 |   77167   283466 |   45681    2055    14763     7.2 | 30.295 % |
c |      3220 |   77022   282975 |   50249    3175    19842     6.2 | 30.419 % |
c |      4928 |   76806   282235 |   55274    4862    32673     6.7 | 30.608 % |
c |      7490 |   76433   280968 |   60802    7356    46587     6.3 | 30.930 % |
c |     11334 |   75920   279231 |   66882   11120    66314     6.0 | 31.386 % |
c |     17100 |   75395   277468 |   73570   16801    97329     5.8 | 31.866 % |
c |     25750 |   74967   276004 |   80927   25393   151397     6.0 | 32.243 % |
c |     38724 |   74305   273766 |   89020   38263   238465     6.2 | 32.818 % |
c |     58186 |   74118   273145 |   97922   57701   404718     7.0 | 32.996 % |
c |     87378 |   73794   272055 |  107714   86838   747619     8.6 | 33.289 % |
c |    131167 |   73547   271210 |  118485   43242   803980    18.6 | 33.507 % |
c |    196851 |   73450   270887 |  130334  108913  2021596    18.6 | 33.596 % |
c |    295377 |   73423   270800 |  143368   99696  1825761    18.3 | 33.626 % |
c |    443166 |   73356   270573 |  157704  127781  2648387    20.7 | 33.685 % |
c ==============================================================================
c [1mFound solution: 5100572[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10697   maxlim: 3644217   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    479053 |  148119   537648 |   49373  163665  3612784    22.1 | 33.685 % |
c |    479153 |  148119   537648 |   54310   33755   330348     9.8 | 22.060 % |
c |    479303 |  148119   537648 |   59741   33905   331227     9.8 | 22.060 % |
c |    479529 |  148119   537648 |   65715   34131   332455     9.7 | 22.060 % |
c |    479866 |  148119   537648 |   72287   34468   334314     9.7 | 22.060 % |
c |    480372 |  148119   537648 |   79515   34974   337592     9.7 | 22.060 % |
c |    481131 |  148119   537648 |   87467   35733   342180     9.6 | 22.060 % |
c |    482270 |  148119   537648 |   96214   36872   349942     9.5 | 22.060 % |
c |    483978 |  148119   537648 |  105835   38580   361613     9.4 | 22.060 % |
c |    486540 |  148119   537648 |  116418   41142   379384     9.2 | 22.060 % |
c |    490384 |  148119   537648 |  128060   44986   416746     9.3 | 22.060 % |
c |    496150 |  148119   537648 |  140866   50752   478078     9.4 | 22.060 % |
c |    504800 |  148119   537648 |  154953   59402   564902     9.5 | 22.060 % |
c |    517774 |  148119   537648 |  170448   72376   723204    10.0 | 22.060 % |
c |    537235 |  148119   537648 |  187493   91837   952676    10.4 | 22.060 % |
c ==============================================================================
c [1mFound solution: 4839776[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3905013   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    549203 |  148150   537902 |   49383  103805  1282446    12.4 | 22.060 % |
c |    549303 |  148150   537902 |   54321   30847   392937    12.7 | 22.092 % |
c |    549453 |  148141   537871 |   59753   30995   393609    12.7 | 22.095 % |
c |    549681 |  148141   537871 |   65728   31223   394991    12.7 | 22.095 % |
c |    550018 |  148141   537871 |   72301   31560   397215    12.6 | 22.095 % |
c |    550524 |  148141   537871 |   79531   32066   400227    12.5 | 22.095 % |
c |    551283 |  148141   537871 |   87484   32825   406301    12.4 | 22.095 % |
c |    552422 |  148141   537871 |   96233   33964   421566    12.4 | 22.095 % |
c |    554130 |  148141   537871 |  105856   35672   436885    12.2 | 22.095 % |
c |    556692 |  148141   537871 |  116442   38234   467993    12.2 | 22.095 % |
c |    560536 |  148141   537871 |  128086   42078   514182    12.2 | 22.095 % |
c |    566302 |  148141   537871 |  140895   47844   616441    12.9 | 22.095 % |
c |    574951 |  148141   537871 |  154985   56493   768859    13.6 | 22.095 % |
c |    587925 |  148135   537851 |  170483   69464  1144594    16.5 | 22.098 % |
c |    607386 |  148135   537851 |  187531   88925  1474260    16.6 | 22.098 % |
c ==============================================================================
c [1mFound solution: 4829338[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 3915451   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    613322 |  148151   538035 |   49383   94861  1541031    16.2 | 22.098 % |
c |    613422 |  148151   538035 |   54321   28511   185525     6.5 | 22.122 % |
c |    613572 |  148127   537953 |   59753   28654   186153     6.5 | 22.135 % |
c |    613797 |  148127   537953 |   65728   28879   187213     6.5 | 22.135 % |
c |    614134 |  148127   537953 |   72301   29216   188959     6.5 | 22.135 % |
c |    614640 |  148127   537953 |   79531   29722   191775     6.5 | 22.135 % |
c |    615399 |  148127   537953 |   87484   30481   195982     6.4 | 22.135 % |
c |    616538 |  148127   537953 |   96233   31620   203679     6.4 | 22.135 % |
c |    618246 |  148127   537953 |  105856   33328   218216     6.5 | 22.135 % |
c |    620809 |  148127   537953 |  116442   35891   247501     6.9 | 22.135 % |
c |    624653 |  148127   537953 |  128086   39735   297403     7.5 | 22.135 % |
c |    630420 |  148127   537953 |  140895   45502   358774     7.9 | 22.135 % |
c |    639074 |  148127   537953 |  154985   54156   541255    10.0 | 22.135 % |
c |    652049 |  148127   537953 |  170483   67131   930758    13.9 | 22.135 % |
c |    671510 |  148127   537953 |  187531   86592  1211056    14.0 | 22.135 % |
c ==============================================================================
c [1mFound solution: 3793680[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 4951109   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    683900 |  148151   538119 |   49383   98982  1387435    14.0 | 22.135 % |
c |    684000 |  148151   538119 |   54321   30093   230824     7.7 | 22.156 % |
c |    684150 |  148151   538119 |   59753   30243   231675     7.7 | 22.156 % |
c |    684375 |  148151   538119 |   65728   30468   232634     7.6 | 22.156 % |
c |    684712 |  148151   538119 |   72301   30805   234353     7.6 | 22.156 % |
c |    685219 |  148151   538119 |   79531   31312   237060     7.6 | 22.156 % |
c |    685978 |  148151   538119 |   87484   32071   240768     7.5 | 22.156 % |
c |    687117 |  148151   538119 |   96233   33210   246246     7.4 | 22.156 % |
c |    688825 |  148151   538119 |  105856   34918   255959     7.3 | 22.156 % |
c |    691387 |  148142   538088 |  116442   37477   271489     7.2 | 22.159 % |
c |    695231 |  148142   538088 |  128086   41321   298820     7.2 | 22.159 % |
c |    700997 |  148142   538088 |  140895   47087   350004     7.4 | 22.159 % |
c |    709647 |  148142   538088 |  154985   55737   450458     8.1 | 22.159 % |
c |    722621 |  148142   538088 |  170483   68711  3010974    43.8 | 22.159 % |
c |    742083 |  148133   538057 |  187531   88170  4687198    53.2 | 22.162 % |
c |    771276 |  148133   538057 |  206285  117363  6015330    51.3 | 22.162 % |
c ==============================================================================
c [1mFound solution: 2703712[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 6041077   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    814000 |  148136   538211 |   49378  160080  6989505    43.7 | 22.162 % |
c |    814100 |  148136   538211 |   54315   32802   449383    13.7 | 22.196 % |
c |    814250 |  148136   538211 |   59747   32952   450058    13.7 | 22.196 % |
c |    814475 |  148136   538211 |   65722   33177   451170    13.6 | 22.196 % |
c |    814812 |  148136   538211 |   72294   33514   453163    13.5 | 22.196 % |
c |    815318 |  148136   538211 |   79523   34020   462971    13.6 | 22.196 % |
c |    816077 |  148136   538211 |   87476   34779   470865    13.5 | 22.196 % |
c |    817217 |  148136   538211 |   96223   35919   481071    13.4 | 22.196 % |
c |    818925 |  148136   538211 |  105846   37627   502543    13.4 | 22.196 % |
c |    821487 |  148136   538211 |  116430   40189   530347    13.2 | 22.196 % |
c |    825331 |  148136   538211 |  128073   44033   577594    13.1 | 22.196 % |
c |    831097 |  148136   538211 |  140881   49799   677022    13.6 | 22.196 % |
c |    839746 |  148136   538211 |  154969   58448   863175    14.8 | 22.196 % |
c |    852722 |  148136   538211 |  170466   71424  1145019    16.0 | 22.196 % |
c |    872184 |  148136   538211 |  187512   90886  3282920    36.1 | 22.196 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 -X3_bit_6 X3_bit_5 X3_bit_4 X3_bit_3 -X3_bit_2 -X3_bit_1 X3_bit0 X3_bit1 -X3_bit2 X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 X5_bit_7 X5_bit_6 X5_bit_5 X5_bit_4 -X5_bit_3 X5_bit_2 -X5_bit_1 -X5_bit0 X5_bit1 X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 X9_bit_7 -X9_bit_6 X9_bit_5 -X9_bit_4 X9_bit_3 X9_bit_2 X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 X10_bit_7 -X10_bit_6 X10_bit_5 X10_bit_4 X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 X11_bit_6 X11_bit_5 X11_bit_4 X11_bit_3 X11_bit_2 X11_bit_1 -X11_bit0 X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 X12_bit_7 X12_bit_6 X12_bit_5 X12_bit_4 X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 X17_bit_7 X17_bit_6 -X17_bit_5 X17_bit_4 -X17_bit_3 X17_bit_2 X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 X18_bit_7 X18_bit_6 -X18_bit_5 X18_bit_4 -X18_bit_3 X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 -X19_bit1 -X19_bit2 X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 X26_bit_6 X26_bit_5 X26_bit_4 X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 X27_bit_7 X27_bit_6 -X27_bit_5 X27_bit_4 X27_bit_3 X27_bit_2 -X27_bit_1 -X27_bit0 X27_bit1 X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 X33_bit_6 X33_bit_5 -X33_bit_4 -X33_bit_3 X33_bit_2 X33_bit_1 X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 X34_bit_6 X34_bit_5 -X34_bit_4 -X34_bit_3 X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 X35_bit_5 X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X37_bit_7 -X37_bit_6 X37_bit_5 X37_bit_4 X37_bit_3 -X37_bit_2 X37_bit_1 -X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 X40_bit_3 -X40_bit_2 X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 -X41_bit_7 -X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 -X41_bit_2 -X41_bit_1 -X41_bit0 -X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 -X43_bit_7 -X43_bit_6 -X43_bit_5 -X43_bit_4 -X43_bit_3 -X43_bit_2 -X43_bit_1 X43_bit0 X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 X44_bit_6 X44_bit_5 -X44_bit_4 X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 -X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 -X48_bit_7 X48_bit_6 -X48_bit_5 X48_bit_4 -X48_bit_3 -X48_bit_2 X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 -X49_bit_5 X49_bit_4 X49_bit_3 -X49_bit_2 X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 -X50_bit_6 -X50_bit_5 -X50_bit_4 -X50_bit_3 -X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 X55_bit_7 -X55_bit_6 -X55_bit_5 -X55_bit_4 -X55_bit_3 -X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 X60_bit_6 X60_bit_5 X60_bit_4 -X60_bit_3 X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 X62_bit_4 -X62_bit_3 X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 X64_bit_6 X64_bit_5 X64_bit_4 X64_bit_3 X64_bit_2 X64_bit_1 X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 X65_bit_6 X65_bit_5 X65_bit_4 X65_bit_3 X65_bit_2 X65_bit_1 X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 -X66_bit_5 X66_bit_4 X66_bit_3 X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 X67_bit_6 -X67_bit_5 X67_bit_4 X67_bit_3 X67_bit_2 X67_bit_1 X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 -X68_bit_7 -X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 X69_bit_6 -X69_bit_5 X69_bit_4 X69_bit_3 X69_bit_2 -X69_bit_1 X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 X70_bit_7 X70_bit_6 X70_bit_5 X70_bit_4 X70_bit_3 X70_bit_2 X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 X72_bit_6 -X72_bit_5 X72_bit_4 X72_bit_3 X72_bit_2 X72_bit_1 X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 -X74_bit_5 -X74_bit_4 -X74_bit_3 -X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 X75_bit_5 -X75_bit_4 X75_bit_3 X75_bit_2 X75_bit_1 -X75_bit0 X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 X76_bit_6 X76_bit_5 -X76_bit_4 X76_bit_3 X76_bit_2 -X76_bit_1 -X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 X77_bit_6 X77_bit_5 -X77_bit_4 X77_bit_3 X77_bit_2 X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 -X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 X79_bit_6 X79_bit_5 -X79_bit_4 X79_bit_3 X79_bit_2 X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 -X81_bit_5 -X81_bit_4 -X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 -X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 -X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 -X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 -X89_bit_1 -X89_bit0 -X89_bit1 X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 X90_bit_6 X90_bit_5 -X90_bit_4 -X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 -X91_bit_7 X91_bit_6 -X91_bit_5 X91_bit_4 -X91_bit_3 -X91_bit_2 -X91_bit_1 X91_bit0 -X91_bit1 X91_bit2 X91_bit3 X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 -X92_bit_5 -X92_bit_4 X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 -X94_bit_7 -X94_bit_6 -X94_bit_5 -X94_bit_4 -X94_bit_3 -X94_bit_2 -X94_bit_1 -X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 X95_bit_7 -X95_bit_6 X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 X96_bit_6 -X96_bit_5 X96_bit_4 X96_bit_3 -X96_bit_2 X96_bit_1 -X96_bit0 X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 X97_bit_6 X97_bit_5 X97_bit_4 X97_bit_3 X97_bit_2 X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 -X98_bit_6 -X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 -X99_bit_7 -X99_bit_6 -X99_bit_5 -X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 -X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 -X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 X101_bit_6 X101_bit_5 X101_bit_4 -X101_bit_3 -X101_bit_2 -X101_bit_1 -X101_bit0 -X101_bit1 X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 X106_bit_6 -X106_bit_5 X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 X107_bit_5 -X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 X108_bit_6 -X108_bit_5 X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 -X111_bit_2 -X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 X114_bit_7 -X114_bit_6 -X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 -X116_bit_7 -X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 X117_bit_6 X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 X119_bit_6 -X119_bit_5 -X119_bit_4 X119_bit_3 X119_bit_2 X119_bit_1 X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 X121_bit_6 X121_bit_5 -X121_bit_4 X121_bit_3 X121_bit_2 -X121_bit_1 X121_bit0 X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 X122_bit_6 -X122_bit_5 X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 -X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 X126_bit1 -X126_bit2 X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 -X128_bit_7 -X128_bit_6 -X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 X129_bit_7 X129_bit_6 X129_bit_5 X129_bit_4 X129_bit_3 X129_bit_2 -X129_bit_1 X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 -X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 -X132_bit_7 -X132_bit_6 -X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 -X134_bit_5 X134_bit_4 -X134_bit_3 -X134_bit_2 -X134_bit_1 -X134_bit0 X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 -X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 X137_bit_6 X137_bit_5 -X137_bit_4 X137_bit_3 X137_bit_2 X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 X138_bit_7 X138_bit_6 X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 X139_bit_2 -X139_bit_1 -X139_bit0 X139_bit1 -X139_bit2 X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 X140_bit_7 X140_bit_6 -X140_bit_5 X140_bit_4 X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 -X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 X145_bit_7 X145_bit_6 X145_bit_5 X145_bit_4 X145_bit_3 X145_bit_2 X145_bit_1 X145_bit0 -X145_bit1 X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 X146_bit_4 X146_bit_3 X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 X147_bit_4 X147_bit_3 X147_bit_2 X147_bit_1 -X147_bit0 X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 X150_bit_6 -X150_bit_5 X150_bit_4 -X150_bit_3 X150_bit_2 X150_bit_1 X150_bit0 X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 X151_bit_6 -X151_bit_5 X151_bit_4 -X151_bit_3 X151_bit_2 X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 X155_bit_5 X155_bit_4 X155_bit_3 X155_bit_2 X155_bit_1 X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 X160_bit_7 X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 X160_bit_2 -X160_bit_1 X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 X161_bit_6 -X161_bit_5 -X161_bit_4 X161_bit_3 X161_bit_2 -X161_bit_1 X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 X163_bit_7 X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 X166_bit_7 X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 X176_bit_6 -X176_bit_5 -X176_bit_4 X176_bit_3 X176_bit_2 X176_bit_1 X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 X179_bit_5 -X179_bit_4 X179_bit_3 X179_bit_2 X179_bit_1 -X179_bit0 X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 -X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 X181_bit_1 X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 X182_bit0 -X182_bit1 X182_bit2 -X182_bit3 X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 X183_bit_6 -X183_bit_5 X183_bit_4 -X183_bit_3 X183_bit_2 -X183_bit_1 X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 -X184_bit_6 X184_bit_5 -X184_bit_4 X184_bit_3 -X184_bit_2 -X184_bit_1 X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 -X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 X188_bit_7 -X188_bit_6 -X188_bit_5 X188_bit_4 X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 -X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 -X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 X194_bit_7 -X194_bit_6 X194_bit_5 -X194_bit_4 X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 X197_bit_7 X197_bit_6 X197_bit_5 -X197_bit_4 X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 X198_bit_1 X198_bit0 X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 X204_bit_6 -X204_bit_5 X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 -X207_bit_4 -X207_bit_3 -X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 X208_bit_6 -X208_bit_5 -X208_bit_4 -X208_bit_3 -X208_bit_2 -X208_bit_1 X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 X211_bit_6 -X211_bit_5 X211_bit_4 X211_bit_3 -X211_bit_2 -X211_bit_1 -X211_bit0 X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 X213_bit_6 -X213_bit_5 -X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 X214_bit_7 X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 X214_bit_2 X214_bit_1 -X214_bit0 X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 X216_bit_7 X216_bit_6 X216_bit_5 -X216_bit_4 X216_bit_3 X216_bit_2 -X216_bit_1 X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 -X217_bit_7 -X217_bit_6 -X217_bit_5 -X217_bit_4 -X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 -X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 X221_bit_7 X221_bit_6 -X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 X222_bit_6 -X222_bit_5 -X222_bit_4 X222_bit_3 X222_bit_2 -X222_bit_1 -X222_bit0 X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 -X226_bit_6 -X226_bit_5 -X226_bit_4 -X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 X227_bit_7 -X227_bit_6 -X227_bit_5 X227_bit_4 X227_bit_3 X227_bit_2 -X227_bit_1 -X227_bit0 X227_bit1 -X227_bit2 -X227_bit3 X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 X229_bit_6 -X229_bit_5 X229_bit_4 X229_bit_3 X229_bit_2 -X229_bit_1 X229_bit0 X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 X230_bit_6 X230_bit_5 X230_bit_4 X230_bit_3 X230_bit_2 -X230_bit_1 -X230_bit0 X230_bit1 X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 X231_bit_7 -X231_bit_6 -X231_bit_5 X231_bit_4 X231_bit_3 X231_bit_2 X231_bit_1 X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 X232_bit_6 X232_bit_5 -X232_bit_4 -X232_bit_3 X232_bit_2 -X232_bit_1 X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 -X233_bit_6 X233_bit_5 -X233_bit_4 -X233_bit_3 X233_bit_2 -X233_bit_1 -X233_bit0 X233_bit1 X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 -X234_bit_5 -X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 -X235_bit_7 -X235_bit_6 -X235_bit_5 -X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 X236_bit_6 -X236_bit_5 X236_bit_4 -X236_bit_3 -X236_bit_2 -X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 -X237_bit_7 -X237_bit_6 -X237_bit_5 -X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 -X241_bit_7 -X241_bit_6 -X241_bit_5 X241_bit_4 -X241_bit_3 X241_bit_2 X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 -X242_bit_7 -X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 X243_bit_7 -X243_bit_6 -X243_bit_5 X243_bit_4 -X243_bit_3 -X243_bit_2 -X243_bit_1 X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 -X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 -X244_bit_3 -X244_bit_2 -X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 -X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 -X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 X248_bit_1 X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 X250_bit_5 -X250_bit_4 -X250_bit_3 X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 X251_bit_5 -X251_bit_4 -X251_bit_3 X251_bit_2 -X251_bit_1 X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 -X252_bit_6 -X252_bit_5 -X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 -X253_bit_6 -X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 -X254_bit_6 X254_bit_5 -X254_bit_4 -X254_bit_3 -X254_bit_2 -X254_bit_1 X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 X255_bit_6 -X255_bit_5 -X255_bit_4 -X255_bit_3 -X255_bit_2 -X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 -Y7_bit0 -Y8_bit0 Y9_bit0 Y10_bit0 Y11_bit0 Y12_bit0 -Y13_bit0 -Y14_bit0 -Y15_bit0 -Y16_bit0 Y17_bit0 Y18_bit0 Y19_bit0 -Y20_bit0 -Y21_bit0 -Y22_bit0 -Y23_bit0 -Y24_bit0 -Y25_bit0 Y26_bit0 Y27_bit0 -Y28_bit0 -Y29_bit0 -Y30_bit0 Y31_bit0 -Y32_bit0 Y33_bit0 Y34_bit0 Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 -Y41_bit0 -Y42_bit0 Y43_bit0 Y44_bit0 Y45_bit0 -Y46_bit0 -Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 -Y51_bit0 Y52_bit0 Y53_bit0 -Y54_bit0 Y55_bit0 -Y56_bit0 -Y57_bit0 -Y58_bit0 Y59_bit0 Y60_bit0 -Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 Y66_bit0 Y67_bit0 -Y68_bit0 Y69_bit0 Y70_bit0 Y71_bit0 Y72_bit0 -Y73_bit0 -Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 -Y78_bit0 Y79_bit0 -Y80_bit0 -Y81_bit0 Y82_bit0 -Y83_bit0 -Y84_bit0 -Y85_bit0 -Y86_bit0 -Y87_bit0 -Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 -Y93_bit0 Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 -Y99_bit0 -Y100_bit0 Y101_bit0 -Y102_bit0 -Y103_bit0 -Y104_bit0 -Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 -Y109_bit0 -Y110_bit0 -Y111_bit0 Y112_bit0 -Y113_bit0 Y#### 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.63 0.89 0.90 2/54 28836
Raw data (stat): 28836 (runsolver) R 28835 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 472777827 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99992 s]
Raw data (loadavg): 0.68 0.89 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2368 0 0 0 991 7 0 0 25 0 1 0 472777827 12013568 2293 4294967295 134512640 134672761 3221224544 3221223728 134559274 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2933 2293 603 41 0 2892 0
vsize: 11732
[startup+20.0013 s]
Raw data (loadavg): 0.73 0.90 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2440 0 0 0 1990 7 0 0 25 0 1 0 472777827 12283904 2365 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2999 2365 603 41 0 2958 0
vsize: 11996
[startup+30.0015 s]
Raw data (loadavg): 0.77 0.90 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2517 0 0 0 2990 7 0 0 25 0 1 0 472777827 12673024 2442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3094 2442 603 41 0 3053 0
vsize: 12376
[startup+40.0023 s]
Raw data (loadavg): 0.81 0.90 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2614 0 0 0 3990 8 0 0 25 0 1 0 472777827 13078528 2539 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3193 2539 603 41 0 3152 0
vsize: 12772
[startup+50.0033 s]
Raw data (loadavg): 0.84 0.91 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2707 0 0 0 4990 8 0 0 25 0 1 0 472777827 13479936 2632 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3291 2632 603 41 0 3250 0
vsize: 13164
[startup+60.0028 s]
Raw data (loadavg): 0.86 0.91 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2800 0 0 0 5990 8 0 0 25 0 1 0 472777827 13877248 2725 4294967295 134512640 134672761 3221224544 3221223668 134566151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3388 2725 603 41 0 3347 0
vsize: 13552
[startup+70.0036 s]
Raw data (loadavg): 0.88 0.91 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2889 0 0 0 6989 9 0 0 25 0 1 0 472777827 14282752 2814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3487 2814 603 41 0 3446 0
vsize: 13948
[startup+80.0037 s]
Raw data (loadavg): 0.90 0.91 0.90 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 2998 0 0 0 7989 9 0 0 25 0 1 0 472777827 14684160 2923 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3585 2923 603 41 0 3544 0
vsize: 14340
[startup+90.0042 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 3157 0 0 0 8989 10 0 0 25 0 1 0 472777827 15351808 3082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3748 3082 603 41 0 3707 0
vsize: 14992
[startup+100.004 s]
Raw data (loadavg): 0.93 0.92 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 3315 0 0 0 9988 10 0 0 25 0 1 0 472777827 15892480 3240 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3880 3240 603 41 0 3839 0
vsize: 15520
[startup+110.004 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 3471 0 0 0 10987 11 0 0 25 0 1 0 472777827 16830464 3396 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4109 3396 603 41 0 4068 0
vsize: 16436
[startup+120.005 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 3660 0 0 0 11987 11 0 0 25 0 1 0 472777827 17506304 3585 4294967295 134512640 134672761 3221224544 3221223696 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4274 3585 603 41 0 4233 0
vsize: 17096
[startup+130.004 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 3826 0 0 0 12987 12 0 0 25 0 1 0 472777827 18182144 3751 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4439 3751 603 41 0 4398 0
vsize: 17756
[startup+140.005 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 4034 0 0 0 13986 13 0 0 25 0 1 0 472777827 18989056 3959 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4636 3959 603 41 0 4595 0
vsize: 18544
[startup+150.005 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 4677 0 0 0 14983 15 0 0 25 0 1 0 472777827 21549056 4602 4294967295 134512640 134672761 3221224544 3221223648 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5261 4602 603 41 0 5220 0
vsize: 21044
[startup+160.005 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5291 0 0 0 15982 17 0 0 25 0 1 0 472777827 24117248 5216 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5888 5216 603 41 0 5847 0
vsize: 23552
[startup+170.005 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 28836
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 16981 17 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+180.006 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 17980 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+190.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 18981 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+200.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 19981 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223792 134562294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+210.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 20981 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+220.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 21981 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+230.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 22982 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+240.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5368 0 0 0 23982 18 0 0 25 0 1 0 472777827 24387584 5293 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5954 5293 603 41 0 5913 0
vsize: 23816
[startup+250.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5499 0 0 0 24982 18 0 0 25 0 1 0 472777827 24928256 5424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6086 5424 603 41 0 6045 0
vsize: 24344
[startup+260.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 5864 0 0 0 25981 19 0 0 25 0 1 0 472777827 26406912 5789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6447 5789 603 41 0 6406 0
vsize: 25788
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6127 0 0 0 26981 19 0 0 25 0 1 0 472777827 27480064 6052 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6709 6052 603 41 0 6668 0
vsize: 26836
[startup+280.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6478 0 0 0 27980 20 0 0 25 0 1 0 472777827 29351936 6403 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7166 6403 603 41 0 7125 0
vsize: 28664
[startup+290.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 28980 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+300.011 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 29980 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+310.011 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 30980 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+320.012 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 31981 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+330.012 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 32981 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+340.012 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 33981 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+350.012 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 34981 20 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+360.012 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 35981 21 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+370.013 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 36981 21 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134564502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+380.013 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 6775 0 0 0 37981 21 0 0 25 0 1 0 472777827 30564352 6700 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7462 6700 603 41 0 7421 0
vsize: 29848
[startup+390.013 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 7596 0 0 0 38979 23 0 0 25 0 1 0 472777827 33939456 7521 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8286 7521 603 41 0 8245 0
vsize: 33144
[startup+400.014 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8209 0 0 0 39978 24 0 0 25 0 1 0 472777827 36503552 8134 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8912 8134 603 41 0 8871 0
vsize: 35648
[startup+410.014 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8314 0 0 0 40978 24 0 0 25 0 1 0 472777827 36909056 8239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9011 8239 603 41 0 8970 0
vsize: 36044
[startup+420.015 s]
Raw data (loadavg): 1.15 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 41978 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+430.016 s]
Raw data (loadavg): 1.12 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 42978 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+440.016 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 43979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223724 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+450.016 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 44979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+460.016 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 45979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+470.017 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 46979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+480.017 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 47979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+490.018 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 48979 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+500.018 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 49980 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+510.018 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 50980 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+520.018 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 51980 24 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+530.018 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 52979 25 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+540.02 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8381 0 0 0 53979 25 0 0 25 0 1 0 472777827 37175296 8306 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8306 603 41 0 9035 0
vsize: 36304
[startup+550.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8386 0 0 0 54979 25 0 0 25 0 1 0 472777827 37175296 8311 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9076 8311 603 41 0 9035 0
vsize: 36304
[startup+560.02 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 8663 0 0 0 55978 25 0 0 25 0 1 0 472777827 38244352 8588 4294967295 134512640 134672761 3221224544 3221215048 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9337 8590 603 41 0 9296 0
vsize: 37348
[startup+570.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9408 0 0 0 56976 28 0 0 25 0 1 0 472777827 41336832 9333 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9333 603 41 0 10051 0
vsize: 40368
[startup+580.021 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9411 0 0 0 57976 28 0 0 25 0 1 0 472777827 41336832 9336 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9336 603 41 0 10051 0
vsize: 40368
[startup+590.022 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9412 0 0 0 58976 28 0 0 25 0 1 0 472777827 41336832 9337 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9337 603 41 0 10051 0
vsize: 40368
[startup+600.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9413 0 0 0 59976 28 0 0 25 0 1 0 472777827 41336832 9338 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9338 603 41 0 10051 0
vsize: 40368
[startup+610.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9414 0 0 0 60977 28 0 0 25 0 1 0 472777827 41336832 9339 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9339 603 41 0 10051 0
vsize: 40368
[startup+620.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9414 0 0 0 61977 28 0 0 25 0 1 0 472777827 41336832 9339 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9339 603 41 0 10051 0
vsize: 40368
[startup+630.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9415 0 0 0 62977 28 0 0 25 0 1 0 472777827 41336832 9340 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9340 603 41 0 10051 0
vsize: 40368
[startup+640.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9415 0 0 0 63977 28 0 0 25 0 1 0 472777827 41336832 9340 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9340 603 41 0 10051 0
vsize: 40368
[startup+650.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9415 0 0 0 64977 28 0 0 25 0 1 0 472777827 41336832 9340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9340 603 41 0 10051 0
vsize: 40368
[startup+660.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9415 0 0 0 65977 28 0 0 25 0 1 0 472777827 41336832 9340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9340 603 41 0 10051 0
vsize: 40368
[startup+670.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9416 0 0 0 66978 28 0 0 25 0 1 0 472777827 41336832 9341 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9341 603 41 0 10051 0
vsize: 40368
[startup+680.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9416 0 0 0 67978 28 0 0 25 0 1 0 472777827 41336832 9341 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10092 9341 603 41 0 10051 0
vsize: 40368
[startup+690.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 68978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+700.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 69978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+710.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 70978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+720.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 71978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+730.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 72978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+740.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 73978 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+750.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 74979 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+760.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 75979 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+770.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9624 0 0 0 76979 29 0 0 25 0 1 0 472777827 41836544 9466 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9466 603 41 0 10173 0
vsize: 40856
[startup+780.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 77979 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+790.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 78979 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 79980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+810.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 80980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+820.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 81980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 82980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+840.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 83980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+850.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 84980 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+860.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9626 0 0 0 85981 29 0 0 25 0 1 0 472777827 41836544 9468 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9468 603 41 0 10173 0
vsize: 40856
[startup+870.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 86981 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 87981 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+890.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 88981 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+900.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 89981 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+910.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 90981 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+920.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 91982 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+930.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 92982 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 93982 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+950.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9629 0 0 0 94982 29 0 0 25 0 1 0 472777827 41836544 9471 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10214 9471 603 41 0 10173 0
vsize: 40856
[startup+960.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 9823 0 0 0 95982 30 0 0 25 0 1 0 472777827 42643456 9665 4294967295 134512640 134672761 3221224544 3221223732 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10411 9665 603 41 0 10370 0
vsize: 41644
[startup+970.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 10344 0 0 0 96981 31 0 0 25 0 1 0 472777827 44789760 10186 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10935 10186 603 41 0 10894 0
vsize: 43740
[startup+980.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 11075 0 0 0 97979 33 0 0 25 0 1 0 472777827 47742976 10917 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11656 10917 603 41 0 11615 0
vsize: 46624
[startup+990.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 11157 0 0 0 98979 33 0 0 25 0 1 0 472777827 48148480 10999 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11755 10999 603 41 0 11714 0
vsize: 47020
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 11727 0 0 0 99978 35 0 0 25 0 1 0 472777827 50446336 11569 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12316 11569 603 41 0 12275 0
vsize: 49264
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 12073 0 0 0 100977 35 0 0 25 0 1 0 472777827 51798016 11915 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12646 11915 603 41 0 12605 0
vsize: 50584
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 12453 0 0 0 101976 36 0 0 25 0 1 0 472777827 53415936 12295 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13041 12295 603 41 0 13000 0
vsize: 52164
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 12561 0 0 0 102976 37 0 0 25 0 1 0 472777827 53817344 12403 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13139 12403 603 41 0 13098 0
vsize: 52556
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 12823 0 0 0 103976 37 0 0 25 0 1 0 472777827 54898688 12665 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13403 12665 603 41 0 13362 0
vsize: 53612
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13034 0 0 0 104975 38 0 0 25 0 1 0 472777827 55844864 12876 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13634 12876 603 41 0 13593 0
vsize: 54536
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13144 0 0 0 105975 38 0 0 25 0 1 0 472777827 56250368 12986 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13733 12986 603 41 0 13692 0
vsize: 54932
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13313 0 0 0 106975 39 0 0 25 0 1 0 472777827 56926208 13155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13898 13155 603 41 0 13857 0
vsize: 55592
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13531 0 0 0 107974 40 0 0 25 0 1 0 472777827 57864192 13373 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14127 13373 603 41 0 14086 0
vsize: 56508
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 108974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 109974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223776 134557473 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 110974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 111974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 112974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13666 0 0 0 113974 40 0 0 25 0 1 0 472777827 58195968 13479 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13479 603 41 0 14167 0
vsize: 56832
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 114975 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 115975 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 116975 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223728 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 117975 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 118975 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28838
Raw data (stat): 28836 (minisat+) R 28835 26667 26666 0 -1 0 13667 0 0 0 119976 40 0 0 25 0 1 0 472777827 58195968 13480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14208 13480 603 41 0 14167 0
vsize: 56832
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 28838
Raw data (stat): 28836 (minisat+) Z 28835 26667 26666 0 -1 12 13670 0 0 0 119976 43 0 0 25 0 1 0 472777827 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.08
CPU time (s): 1200.21
CPU user time (s): 1199.77
CPU system time (s): 0.436933
CPU usage (%): 100.01
Max. virtual memory (Kb): 56832
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####