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-ran17x17.opb
MD5SUM	4afffa77a031423497a8b9b377dd0292
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	689314
Optimality of the best value was proved	NO
Number of terms in the objective function	6069
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	1576985250
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	1576985250
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	6069
Total number of constraints	323
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	323
Minimum length of a constraint	21
Maximum length of a constraint	340
Trace number 17628

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        512672 kB
Buffers:         17332 kB
Cached:         478488 kB
SwapCached:        512 kB
Active:         114912 kB
Inactive:       382916 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        512420 kB
SwapTotal:     2097892 kB
SwapFree:      2096484 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            18516 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:21:22 (client local time) WITH STATUS 10 IN 1200.43 SECONDS
stats: 19330 7 1200.43 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 357 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 355]---> BDD-cost: 2836
c ---[ 353]---> BDD-cost: 2423
c ---[ 351]---> BDD-cost: 2913
c ---[ 349]---> BDD-cost: 2728
c ---[ 347]---> BDD-cost: 3308
c ---[ 345]---> BDD-cost: 2667
c ---[ 343]---> BDD-cost: 2619
c ---[ 341]---> BDD-cost: 3308
c ---[ 339]---> BDD-cost: 3410
c ---[ 337]---> BDD-cost: 3179
c ---[ 335]---> BDD-cost: 3241
c ---[ 333]---> BDD-cost: 2937
c ---[ 331]---> BDD-cost: 3394
c ---[ 329]---> BDD-cost: 3271
c ---[ 327]---> BDD-cost: 3084
c ---[ 325]---> BDD-cost: 2313
c ---[ 323]---> BDD-cost: 2204
c ---[ 321]---> BDD-cost: 3047
c ---[ 319]---> BDD-cost: 2427
c ---[ 317]---> BDD-cost: 2627
c ---[ 315]---> BDD-cost: 2208
c ---[ 313]---> BDD-cost: 2947
c ---[ 311]---> BDD-cost: 3031
c ---[ 309]---> BDD-cost: 2846
c ---[ 307]---> BDD-cost: 3411
c ---[ 305]---> BDD-cost: 3093
c ---[ 303]---> BDD-cost: 2010
c ---[ 301]---> BDD-cost: 3140
c ---[ 299]---> BDD-cost: 3279
c ---[ 297]---> BDD-cost: 3190
c ---[ 295]---> BDD-cost: 3459
c ---[ 293]---> BDD-cost: 3348
c ---[ 291]---> BDD-cost: 2010
c ---[ 289]---> BDD-cost: 3328
c ---[ 288]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   12
c ---[ 286]---> BDD-cost:   12
c ---[ 285]---> BDD-cost:   14
c ---[ 284]---> BDD-cost:   17
c ---[ 283]---> BDD-cost:   17
c ---[ 282]---> BDD-cost:   12
c ---[ 281]---> BDD-cost:   11
c ---[ 280]---> BDD-cost:   15
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   17
c ---[ 277]---> BDD-cost:   17
c ---[ 276]---> BDD-cost:   17
c ---[ 275]---> BDD-cost:   11
c ---[ 274]---> BDD-cost:   11
c ---[ 273]---> BDD-cost:   17
c ---[ 272]---> BDD-cost:   12
c ---[ 271]---> BDD-cost:   11
c ---[ 270]---> BDD-cost:   15
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   17
c ---[ 266]---> BDD-cost:   17
c ---[ 265]---> BDD-cost:   17
c ---[ 264]---> BDD-cost:   13
c ---[ 263]---> BDD-cost:   12
c ---[ 262]---> BDD-cost:   11
c ---[ 261]---> BDD-cost:   17
c ---[ 260]---> BDD-cost:   17
c ---[ 259]---> BDD-cost:   17
c ---[ 258]---> BDD-cost:   17
c ---[ 257]---> BDD-cost:   17
c ---[ 256]---> BDD-cost:   11
c ---[ 255]---> BDD-cost:   17
c ---[ 254]---> BDD-cost:   12
c ---[ 253]---> BDD-cost:   13
c ---[ 252]---> BDD-cost:   11
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   17
c ---[ 247]---> BDD-cost:   17
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   11
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   13
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   11
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   11
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   13
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   11
c ---[ 226]---> BDD-cost:   11
c ---[ 225]---> BDD-cost:   11
c ---[ 224]---> BDD-cost:   11
c ---[ 223]---> BDD-cost:   11
c ---[ 222]---> BDD-cost:   11
c ---[ 221]---> BDD-cost:   11
c ---[ 220]---> BDD-cost:   13
c ---[ 219]---> BDD-cost:   11
c ---[ 218]---> BDD-cost:   11
c ---[ 217]---> BDD-cost:   11
c ---[ 216]---> BDD-cost:   11
c ---[ 215]---> BDD-cost:   11
c ---[ 214]---> BDD-cost:   11
c ---[ 213]---> BDD-cost:   11
c ---[ 212]---> BDD-cost:   11
c ---[ 211]---> BDD-cost:   11
c ---[ 210]---> BDD-cost:   11
c ---[ 209]---> BDD-cost:   12
c ---[ 208]---> BDD-cost:   14
c ---[ 207]---> BDD-cost:   12
c ---[ 206]---> BDD-cost:   11
c ---[ 205]---> BDD-cost:   14
c ---[ 204]---> BDD-cost:   14
c ---[ 203]---> BDD-cost:   14
c ---[ 202]---> BDD-cost:   14
c ---[ 201]---> BDD-cost:   14
c ---[ 200]---> BDD-cost:   11
c ---[ 199]---> BDD-cost:   14
c ---[ 198]---> BDD-cost:   12
c ---[ 197]---> BDD-cost:   12
c ---[ 196]---> BDD-cost:   11
c ---[ 195]---> BDD-cost:   14
c ---[ 194]---> BDD-cost:   14
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   14
c ---[ 191]---> BDD-cost:   14
c ---[ 190]---> BDD-cost:   14
c ---[ 189]---> BDD-cost:   12
c ---[ 188]---> BDD-cost:   11
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:   14
c ---[ 185]---> BDD-cost:   14
c ---[ 184]---> BDD-cost:   14
c ---[ 183]---> BDD-cost:   14
c ---[ 182]---> BDD-cost:   14
c ---[ 181]---> BDD-cost:   11
c ---[ 180]---> BDD-cost:   14
c ---[ 179]---> BDD-cost:   12
c ---[ 178]---> BDD-cost:   11
c ---[ 177]---> BDD-cost:   14
c ---[ 176]---> BDD-cost:   11
c ---[ 175]---> BDD-cost:   12
c ---[ 174]---> BDD-cost:   14
c ---[ 173]---> BDD-cost:   14
c ---[ 172]---> BDD-cost:   14
c ---[ 171]---> BDD-cost:   14
c ---[ 170]---> BDD-cost:   17
c ---[ 169]---> BDD-cost:   12
c ---[ 168]---> BDD-cost:   11
c ---[ 167]---> BDD-cost:   15
c ---[ 166]---> BDD-cost:   16
c ---[ 165]---> BDD-cost:   17
c ---[ 164]---> BDD-cost:   12
c ---[ 163]---> BDD-cost:   15
c ---[ 162]---> BDD-cost:   15
c ---[ 161]---> BDD-cost:   11
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   12
c ---[ 158]---> BDD-cost:   11
c ---[ 157]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   15
c ---[ 153]---> BDD-cost:   12
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   15
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   11
c ---[ 148]---> BDD-cost:   15
c ---[ 147]---> BDD-cost:   15
c ---[ 146]---> BDD-cost:   15
c ---[ 145]---> BDD-cost:   15
c ---[ 144]---> BDD-cost:   15
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:   12
c ---[ 141]---> BDD-cost:   15
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:   15
c ---[ 136]---> BDD-cost:   15
c ---[ 135]---> BDD-cost:   15
c ---[ 134]---> BDD-cost:   15
c ---[ 133]---> BDD-cost:   12
c ---[ 132]---> BDD-cost:   12
c ---[ 131]---> BDD-cost:   12
c ---[ 130]---> BDD-cost:   11
c ---[ 129]---> BDD-cost:   12
c ---[ 128]---> BDD-cost:   12
c ---[ 127]---> BDD-cost:   12
c ---[ 126]---> BDD-cost:   12
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   11
c ---[ 123]---> BDD-cost:   12
c ---[ 122]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:   11
c ---[ 120]---> BDD-cost:   11
c ---[ 119]---> BDD-cost:   12
c ---[ 118]---> BDD-cost:   12
c ---[ 117]---> BDD-cost:   12
c ---[ 116]---> BDD-cost:   12
c ---[ 115]---> BDD-cost:   12
c ---[ 114]---> BDD-cost:   17
c ---[ 113]---> BDD-cost:   12
c ---[ 112]---> BDD-cost:   11
c ---[ 111]---> BDD-cost:   15
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   12
c ---[ 108]---> BDD-cost:   17
c ---[ 107]---> BDD-cost:   15
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   11
c ---[ 104]---> BDD-cost:   15
c ---[ 103]---> BDD-cost:   12
c ---[ 102]---> BDD-cost:   11
c ---[ 101]---> BDD-cost:   15
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> BDD-cost:   12
c ---[  97]---> BDD-cost:   15
c ---[  96]---> BDD-cost:   17
c ---[  95]---> BDD-cost:   17
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   11
c ---[  92]---> BDD-cost:   15
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:   16
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:   11
c ---[  85]---> BDD-cost:   17
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:   11
c ---[  82]---> BDD-cost:   15
c ---[  81]---> BDD-cost:   13
c ---[  80]---> BDD-cost:   13
c ---[  79]---> BDD-cost:   19
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:   12
c ---[  76]---> BDD-cost:   13
c ---[  75]---> BDD-cost:   12
c ---[  74]---> BDD-cost:   12
c ---[  73]---> BDD-cost:   12
c ---[  72]---> BDD-cost:   12
c ---[  71]---> BDD-cost:   17
c ---[  70]---> BDD-cost:   12
c ---[  69]---> BDD-cost:   11
c ---[  68]---> BDD-cost:   15
c ---[  67]---> BDD-cost:   17
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   13
c ---[  64]---> BDD-cost:   17
c ---[  63]---> BDD-cost:   17
c ---[  62]---> BDD-cost:   11
c ---[  61]---> BDD-cost:   17
c ---[  60]---> BDD-cost:   12
c ---[  59]---> BDD-cost:   11
c ---[  58]---> BDD-cost:   15
c ---[  57]---> BDD-cost:   13
c ---[  56]---> BDD-cost:   13
c ---[  55]---> BDD-cost:   17
c ---[  54]---> BDD-cost:   13
c ---[  53]---> BDD-cost:   17
c ---[  52]---> BDD-cost:   17
c ---[  51]---> BDD-cost:   12
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   15
c ---[  48]---> BDD-cost:   17
c ---[  47]---> BDD-cost:   17
c ---[  46]---> BDD-cost:   17
c ---[  45]---> BDD-cost:   17
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   13
c ---[  42]---> BDD-cost:   17
c ---[  41]---> BDD-cost:   12
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   15
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   17
c ---[  35]---> BDD-cost:   17
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   12
c ---[  32]---> BDD-cost:   13
c ---[  31]---> BDD-cost:   11
c ---[  30]---> BDD-cost:   15
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   15
c ---[  27]---> BDD-cost:   15
c ---[  26]---> BDD-cost:   15
c ---[  25]---> BDD-cost:   11
c ---[  24]---> BDD-cost:   15
c ---[  23]---> BDD-cost:   12
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:   11
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   15
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   15
c ---[  16]---> BDD-cost:   15
c ---[  15]---> BDD-cost:   17
c ---[  14]---> BDD-cost:   12
c ---[  13]---> BDD-cost:   11
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   16
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:   17
c ---[   8]---> BDD-cost:   14
c ---[   7]---> BDD-cost:   16
c ---[   6]---> BDD-cost:   11
c ---[   5]---> BDD-cost:   17
c ---[   4]---> BDD-cost:   12
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  292444   854642 |   97481       0        0     nan |  0.000 % |
c |       100 |  292444   854642 |  107229     100     4776    47.8 |  2.804 % |
c |       250 |  292444   854642 |  117952     250     9498    38.0 |  2.804 % |
c |       475 |  292444   854642 |  129747     475    30406    64.0 |  2.804 % |
c ==============================================================================
c [1mFound solution: 1799070[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:581119     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       722 | 1875565  4548808 |  625188     722    38565    53.4 |  2.804 % |
c |       822 | 1875479  4548614 |  687706     820    45827    55.9 |  0.453 % |
c |       972 | 1875479  4548614 |  756477     970    46590    48.0 |  0.453 % |
c |      1197 | 1875479  4548614 |  832125    1195    47732    39.9 |  0.453 % |
c |      1535 | 1874923  4547357 |  915337    1523    57253    37.6 |  0.475 % |
c |      2041 | 1874923  4547357 | 1006871    2029    65098    32.1 |  0.475 % |
c |      2801 | 1874554  4546520 | 1107558    2774    69541    25.1 |  0.491 % |
c |      3940 | 1874554  4546520 | 1218314    3913    77792    19.9 |  0.491 % |
c |      5649 | 1874481  4546355 | 1340146    5621   100920    18.0 |  0.494 % |
c |      8212 | 1874481  4546355 | 1474160    8184   128130    15.7 |  0.494 % |
c |     12056 | 1874481  4546355 | 1621576   12028   179699    14.9 |  0.494 % |
c |     17822 | 1874481  4546355 | 1783734   17794   256851    14.4 |  0.494 % |
c |     26472 | 1874269  4545876 | 1962107   26442   391086    14.8 |  0.503 % |
c |     39446 | 1874208  4545738 | 2158318   39415   936986    23.8 |  0.505 % |
c |     58907 | 1872590  4542048 | 2374150   58862  1783568    30.3 |  0.576 % |
c |     88099 | 1872590  4542048 | 2611565   88054  2513611    28.5 |  0.576 % |
c ==============================================================================
c [1mFound solution: 1794355[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    9     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103134 | 1871835  4542776 |  623945  103078  3116104    30.2 |  0.576 % |
c |    103234 | 1871355  4541679 |  686339  103175  3116608    30.2 |  0.631 % |
c |    103384 | 1870954  4540759 |  754973  103320  3117457    30.2 |  0.650 % |
c |    103610 | 1868775  4535750 |  830470  103515  3119884    30.1 |  0.750 % |
c |    103947 | 1868775  4535750 |  913517  103852  3122675    30.1 |  0.750 % |
c |    104453 | 1868775  4535750 | 1004869  104358  3125757    30.0 |  0.750 % |
c |    105212 | 1868775  4535750 | 1105356  105117  3135131    29.8 |  0.750 % |
c |    106351 | 1868775  4535750 | 1215892  106256  3150931    29.7 |  0.750 % |
c |    108059 | 1868675  4535522 | 1337481  107963  3189546    29.5 |  0.755 % |
c |    110621 | 1868675  4535522 | 1471229  110525  3293032    29.8 |  0.755 % |
c |    114465 | 1868675  4535522 | 1618352  114369  3630448    31.7 |  0.755 % |
c |    120231 | 1868675  4535522 | 1780187  120135  3840864    32.0 |  0.755 % |
c |    128883 | 1868675  4535522 | 1958206  128787  4012142    31.2 |  0.755 % |
c |    141857 | 1868675  4535522 | 2154027  141761  4614407    32.6 |  0.755 % |
c |    161318 | 1867934  4533821 | 2369430  161214  5242336    32.5 |  0.789 % |
c |    190510 | 1867934  4533821 | 2606373  190406  6021872    31.6 |  0.789 % |
c |    234301 | 1863914  4524583 | 2867010  234135  9275667    39.6 |  0.974 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 X12_bit1 -X12_bit2 -X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 -X15_bit_6 -X15_bit_5 -X15_bit_4 -X15_bit_3 -X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 -X17_bit_3 -X17_bit_2 -X17_bit_1 -X17_bit0 -X17_bit1 -X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 -X19_bit_7 -X19_bit_6 -X19_bit_5 -X19_bit_4 -X19_bit_3 -X19_bit_2 -X19_bit_1 -X19_bit0 X19_bit1 -X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 -X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 -X21_bit_6 -X21_bit_5 -X21_bit_4 -X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 -X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 -X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 -X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 X34_bit_5 X34_bit_4 -X34_bit_3 X34_bit_2 X34_bit_1 X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 X37_bit_6 X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 X38_bit_6 X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X39_bit_7 -X39_bit_6 -X39_bit_5 X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 X40_bit_7 -X40_bit_6 X40_bit_5 X40_bit_4 X40_bit_3 X40_bit_2 X40_bit_1 X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 X41_bit_5 X41_bit_4 -X41_bit_3 -X41_bit_2 X41_bit_1 X41_bit0 -X41_bit1 X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 -X42_bit_6 -X42_bit_5 -X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 X43_bit_6 X43_bit_5 X43_bit_4 X43_bit_3 -X43_bit_2 X43_bit_1 X43_bit0 X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 -X44_bit_7 -X44_bit_6 -X44_bit_5 -X44_bit_4 -X44_bit_3 -X44_bit_2 -X44_bit_1 -X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 -X45_bit_7 -X45_bit_6 -X45_bit_5 -X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 -X46_bit_7 -X46_bit_6 X46_bit_5 -X46_bit_4 -X46_bit_3 -X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 X47_bit_7 X47_bit_6 -X47_bit_5 X47_bit_4 -X47_bit_3 X47_bit_2 X47_bit_1 X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 X48_bit_7 -X48_bit_6 X48_bit_5 -X48_bit_4 -X48_bit_3 -X48_bit_2 -X48_bit_1 X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 X49_bit_7 X49_bit_6 X49_bit_5 X49_bit_4 X49_bit_3 -X49_bit_2 -X49_bit_1 X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 X50_bit_6 X50_bit_5 X50_bit_4 X50_bit_3 X50_bit_2 X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 X51_bit_7 -X51_bit_6 X51_bit_5 -X51_bit_4 -X51_bit_3 X51_bit_2 X51_bit_1 X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 -X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 -X53_bit_7 -X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 X54_bit_7 X54_bit_6 X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 X54_bit0 X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 X55_bit_7 -X55_bit_6 X55_bit_5 X55_bit_4 -X55_bit_3 X55_bit_2 -X55_bit_1 X55_bit0 -X55_bit1 X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 -X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 -X56_bit_3 -X56_bit_2 -X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 X57_bit_7 X57_bit_6 -X57_bit_5 X57_bit_4 -X57_bit_3 X57_bit_2 X57_bit_1 X57_bit0 -X57_bit1 X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 X60_bit_7 -X60_bit_6 X60_bit_5 X60_bit_4 X60_bit_3 X60_bit_2 -X60_bit_1 X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 -X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 -X62_bit_6 -X62_bit_5 -X62_bit_4 -X62_bit_3 -X62_bit_2 -X62_bit_1 -X62_bit0 X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 -X64_bit_6 X64_bit_5 X64_bit_4 X64_bit_3 -X64_bit_2 X64_bit_1 X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 X65_bit_7 X65_bit_6 X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 -X66_bit_7 -X66_bit_6 -X66_bit_5 X66_bit_4 X66_bit_3 -X66_bit_2 X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 X67_bit_6 X67_bit_5 X67_bit_4 X67_bit_3 X67_bit_2 -X67_bit_1 -X67_bit0 -X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 -X68_bit_6 X68_bit_5 -X68_bit_4 X68_bit_3 -X68_bit_2 -X68_bit_1 -X68_bit0 X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 -X69_bit_7 -X69_bit_6 -X69_bit_5 -X69_bit_4 -X69_bit_3 -X69_bit_2 -X69_bit_1 -X69_bit0 -X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 -X70_bit_7 -X70_bit_6 -X70_bit_5 -X70_bit_4 -X70_bit_3 -X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 X71_bit_7 X71_bit_6 X71_bit_5 X71_bit_4 -X71_bit_3 X71_bit_2 X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 X72_bit_6 -X72_bit_5 X72_bit_4 -X72_bit_3 X72_bit_2 -X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 X74_bit_7 X74_bit_6 -X74_bit_5 X74_bit_4 -X74_bit_3 X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 X75_bit_6 X75_bit_5 X75_bit_4 -X75_bit_3 X75_bit_2 -X75_bit_1 -X75_bit0 -X75_bit1 X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 -X76_bit_7 -X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 -X76_bit_2 -X76_bit_1 X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 X77_bit_7 -X77_bit_6 -X77_bit_5 X77_bit_4 -X77_bit_3 -X77_bit_2 X77_bit_1 X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 -X78_bit_7 -X78_bit_6 -X78_bit_5 -X78_bit_4 -X78_bit_3 -X78_bit_2 X78_bit_1 -X78_bit0 -X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 -X79_bit_5 -X79_bit_4 -X79_bit_3 -X79_bit_2 -X79_bit_1 -X79_bit0 -X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 X81_bit_7 -X81_bit_6 X81_bit_5 -X81_bit_4 X81_bit_3 -X81_bit_2 -X81_bit_1 -X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 X82_bit_6 X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 X83_bit_6 -X83_bit_5 X83_bit_4 -X83_bit_3 -X83_bit_2 X83_bit_1 X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 X84_bit_7 -X84_bit_6 -X84_bit_5 -X84_bit_4 -X84_bit_3 -X84_bit_2 -X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 X85_bit_6 X85_bit_5 X85_bit_4 X85_bit_3 -X85_bit_2 -X85_bit_1 -X85_bit0 X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 X88_bit_7 X88_bit_6 X88_bit_5 X88_bit_4 -X88_bit_3 -X88_bit_2 X88_bit_1 X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 X89_bit_6 X89_bit_5 X89_bit_4 -X89_bit_3 -X89_bit_2 -X89_bit_1 -X89_bit0 X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 X90_bit_7 -X90_bit_6 -X90_bit_5 X90_bit_4 -X90_bit_3 X90_bit_2 X90_bit_1 -X90_bit0 X90_bit1 -X90_bit2 X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 X91_bit_6 X91_bit_5 X91_bit_4 X91_bit_3 X91_bit_2 X91_bit_1 -X91_bit0 -X91_bit1 -X91_bit2 -X91_bit3 -X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 X92_bit_5 X92_bit_4 -X92_bit_3 -X92_bit_2 -X92_bit_1 -X92_bit0 X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 -X93_bit_7 -X93_bit_6 -X93_bit_5 -X93_bit_4 -X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 X94_bit_6 -X94_bit_5 X94_bit_4 -X94_bit_3 -X94_bit_2 X94_bit_1 X94_bit0 -X94_bit1 -X94_bit2 -X94_bit3 -X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 X95_bit_1 X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 -X96_bit_7 -X96_bit_6 -X96_bit_5 -X96_bit_4 -X96_bit_3 -X96_bit_2 -X96_bit_1 X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 X97_bit_5 -X97_bit_4 -X97_bit_3 X97_bit_2 -X97_bit_1 -X97_bit0 X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 X98_bit_6 -X98_bit_5 X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 X99_bit_6 -X99_bit_5 X99_bit_4 -X99_bit_3 -X99_bit_2 -X99_bit_1 X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 -X100_bit_7 X100_bit_6 -X100_bit_5 X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 X101_bit_7 X101_bit_6 X101_bit_5 X101_bit_4 X101_bit_3 X101_bit_2 -X101_bit_1 -X101_bit0 X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 X102_bit_6 X102_bit_5 X102_bit_4 X102_bit_3 -X102_bit_2 X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 -X104_bit_7 -X104_bit_6 -X104_bit_5 -X104_bit_4 -X104_bit_3 -X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 -X105_bit_7 -X105_bit_6 -X105_bit_5 -X105_bit_4 -X105_bit_3 -X105_bit_2 -X105_bit_1 -X105_bit0 -X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 X106_bit_7 X106_bit_6 -X106_bit_5 X106_bit_4 X106_bit_3 X106_bit_2 X106_bit_1 X106_bit0 -X106_bit1 X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 X107_bit_7 -X107_bit_6 X107_bit_5 X107_bit_4 -X107_bit_3 -X107_bit_2 -X107_bit_1 -X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 X108_bit_7 X108_bit_6 X108_bit_5 -X108_bit_4 X108_bit_3 -X108_bit_2 X108_bit_1 X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 X109_bit_6 X109_bit_5 X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 X109_bit0 X109_bit1 X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 X111_bit_7 X111_bit_6 -X111_bit_5 X111_bit_4 -X111_bit_3 X111_bit_2 -X111_bit_1 X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 -X112_bit_5 -X112_bit_4 -X112_bit_3 -X112_bit_2 -X112_bit_1 X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 -X114_bit_5 X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 X115_bit_7 -X115_bit_6 X115_bit_5 X115_bit_4 X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 -X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 -X116_bit_6 X116_bit_5 -X116_bit_4 X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 X117_bit_7 -X117_bit_6 -X117_bit_5 X117_bit_4 X117_bit_3 -X117_bit_2 X117_bit_1 -X117_bit0 X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 X118_bit_7 X118_bit_6 X118_bit_5 -X118_bit_4 X118_bit_3 X118_bit_2 X118_bit_1 X118_bit0 X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 -X119_bit_6 X119_bit_5 -X119_bit_4 -X119_bit_3 -X119_bit_2 -X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 X122_bit_6 X122_bit_5 X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 X124_bit_7 X124_bit_6 X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 X125_bit_7 X125_bit_6 X125_bit_5 X125_bit_4 -X125_bit_3 X125_bit_2 X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 X126_bit_7 -X126_bit_6 -X126_bit_5 X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 X128_bit_7 X128_bit_6 -X128_bit_5 X128_bit_4 -X128_bit_3 -X128_bit_2 -X128_bit_1 X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 -X129_bit_7 -X129_bit_6 -X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 -X129_bit_1 -X129_bit0 -X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 -X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 -X131_bit_7 -X131_bit_6 -X131_bit_5 X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 -X132_bit_6 -X132_bit_5 X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 X133_bit_5 -X133_bit_4 X133_bit_3 -X133_bit_2 X133_bit_1 X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 X134_bit_7 X134_bit_6 X134_bit_5 X134_bit_4 -X134_bit_3 X134_bit_2 X134_bit_1 X134_bit0 X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 X135_bit_7 X135_bit_6 X135_bit_5 X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 -X136_bit_7 -X136_bit_6 -X136_bit_5 -X136_bit_4 -X136_bit_3 X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 -X137_bit_7 -X137_bit_6 -X137_bit_5 -X137_bit_4 -X137_bit_3 -X137_bit_2 -X137_bit_1 -X137_bit0 -X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 -X138_bit_7 -X138_bit_6 -X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 -X139_bit_7 -X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 -X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 -X140_bit_7 -X140_bit_6 -X140_bit_5 -X140_bit_4 X140_bit_3 -X140_bit_2 -X140_bit_1 -X140_bit0 -X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 -X141_bit_7 -X141_bit_6 -X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 -X142_bit_7 -X142_bit_6 X142_bit_5 -X142_bit_4 -X142_bit_3 -X142_bit_2 X142_bit_1 X142_bit0 -X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 X145_bit_7 -X145_bit_6 -X145_bit_5 X145_bit_4 -X145_bit_3 -X145_bit_2 -X145_bit_1 X145_bit0 -X145_bit1 -X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 -X146_bit_7 -X146_bit_6 -X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 -X147_bit_6 -X147_bit_5 -X147_bit_4 -X147_bit_3 -X147_bit_2 -X147_bit_1 -X147_bit0 -X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 -X148_bit_7 -X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 X150_bit_7 X150_bit_6 -X150_bit_5 X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 -X151_bit_7 -X151_bit_6 -X151_bit_5 X151_bit_4 -X151_bit_3 -X151_bit_2 X151_bit_1 -X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 -X152_bit_3 X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 -X155_bit_7 -X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 -X155_bit0 -X155_bit1 -X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 -X157_bit_7 -X157_bit_6 -X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 -X159_bit_7 -X159_bit_6 -X159_bit_5 -X159_bit_4 -X159_bit_3 -X159_bit_2 -X159_bit_1 -X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 -X160_bit_7 -X160_bit_6 -X160_bit_5 -X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 X160_bit0 -X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 -X161_bit_7 -X161_bit_6 -X161_bit_5 -X161_bit_4 -X161_bit_3 -X161_bit_2 -X161_bit_1 X161_bit0 -X161_bit1 -X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 -X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 -X167_bit_7 -X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 -X167_bit_2 -X167_bit_1 -X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 -X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 X170_bit_2 -X170_bit_1 -X170_bit0 X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 -X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 X173_bit_2 -X173_bit_1 -X173_bit0 X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 X174_bit_5 -X174_bit_4 -X174_bit_3 X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 X175_bit_7 -X175_bit_6 -X175_bit_5 -X175_bit_4 -X175_bit_3 -X175_bit_2 -X175_bit_1 -X175_bit0 -X175_bit1 -X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 X176_bit_7 -X176_bit_6 X176_bit_5 -X176_bit_4 -X176_bit_3 -X176_bit_2 X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 X177_bit_2 -X177_bit_1 -X177_bit0 X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 -X178_bit_7 -X178_bit_6 -X178_bit_5 -X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 -X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 -X179_bit_5 -X179_bit_4 -X179_bit_3 -X179_bit_2 -X179_bit_1 -X179_bit0 -X179_bit1 -X179_bit2 -X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 -X180_bit_7 -X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 -X181_bit_6 -X181_bit_5 -X181_bit_4 -X181_bit_3 -X181_bit_2 -X181_bit_1 -X181_bit0 -X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 -X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 -X182_bit_3 -X182_bit_2 -X182_bit_1 X182_bit0 -X182_bit1 -X182_bit2 -X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 X183_bit_7 -X183_bit_6 -X183_bit_5 X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 X184_bit_7 -X184_bit_6 -X184_bit_5 X184_bit_4 -X184_bit_3 -X184_bit_2 X184_bit_1 X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 X186_bit_5 -X186_bit_4 -X186_bit_3 X186_bit_2 X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 -X187_bit_7 -X187_bit_6 -X187_bit_5 X187_bit_4 -X187_bit_3 -X187_bit_2 -X187_bit_1 -X187_bit0 -X187_bit1 -X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 -X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 -X191_bit_7 -X191_bit_6 -X191_bit_5 -X191_bit_4 -X191_bit_3 -X191_bit_2 -X191_bit_1 X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 -X192_bit_7 -X192_bit_6 X192_bit_5 -X192_bit_4 -X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 -X193_bit_5 -X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 -X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 -X195_bit_7 -X195_bit_6 -X195_bit_5 -X195_bit_4 -X195_bit_3 -X195_bit_2 -X195_bit_1 -X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 -X197_bit_6 -X197_bit_5 -X197_bit_4 -X197_bit_3 -X197_bit_2 -X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 -X198_bit_7 -X198_bit_6 -X198_bit_5 -X198_bit_4 -X198_bit_3 -X198_bit_2 -X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 -X199_bit_7 -X199_bit_6 -X199_bit_5 -X199_bit_4 -X199_bit_3 -X199_bit_2 -X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 -X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 X200_bit_3 -X200_bit_2 -X200_bit_1 X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 -X202_bit_7 -X202_bit_6 -X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 X202_bit0 X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 X204_bit_6 X204_bit_5 -X204_bit_4 X204_bit_3 X204_bit_2 X204_bit_1 X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 -X205_bit_7 -X205_bit_6 -X205_bit_5 -X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 -X206_bit_7 -X206_bit_6 -X206_bit_5 -X206_bit_4 -X206_bit_3 -X206_bit_2 -X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 -X207_bit_5 X207_bit_4 -X207_bit_3 X207_bit_2 -X207_bit_1 X207_bit0 X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 -X208_bit_7 X208_bit_6 X208_bit_5 X208_bit_4 X208_bit_3 X208_bit_2 X208_bit_1 X208_bit0 X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 X209_bit_7 -X209_bit_6 X209_bit_5 X209_bit_4 -X209_bit_3 X209_bit_2 X209_bit_1 X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 X210_bit_7 X210_bit_6 -X210_bit_5 X210_bit_4 X210_bit_3 X210_bit_2 -X210_bit_1 X210_bit0 X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 X211_bit_6 -X211_bit_5 X211_bit_4 X211_bit_3 X211_bit_2 X211_bit_1 -X211_bit0 X211_bit1 -X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 -X212_bit_7 -X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 X213_bit_7 X213_bit_6 X213_bit_5 X213_bit_4 X213_bit_3 -X213_bit_2 -X213_bit_1 X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 -X215_bit_7 -X215_bit_6 -X215_bit_5 -X215_bit_4 -X215_bit_3 -X215_bit_2 -X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 X216_bit_5 -X216_bit_4 -X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 -X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 X217_bit_6 X217_bit_5 -X217_bit_4 X217_bit_3 -X217_bit_2 -X217_bit_1 -X217_bit0 -X217_bit1 X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 X218_bit_7 -X218_bit_6 X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 X219_bit_7 -X219_bit_6 X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 X219_bit_1 X219_bit0 X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 X220_bit_6 X220_bit_5 X220_bit_4 X220_bit_3 X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 X221_bit_6 X221_bit_5 X221_bit_4 -X221_bit_3 X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 -X224_bit_7 X224_bit_6 X224_bit_5 X224_bit_4 -X224_bit_3 -X224_bit_2 -X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 -X226_bit_6 -X226_bit_5 -X226_bit_4 -X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 X227_bit_6 X227_bit_5 X227_bit_4 -X227_bit_3 X227_bit_2 -X227_bit_1 -X227_bit0 X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 X228_bit_7 X228_bit_6 X228_bit_5 X228_bit_4 -X228_bit_3 X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 -X229_bit_7 -X229_bit_6 -X229_bit_5 -X229_bit_4 -X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 -X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 X230_bit_7 -X230_bit_6 -X230_bit_5 X230_bit_4 -X230_bit_3 -X230_bit_2 -X230_bit_1 X230_bit0 -X230_bit1 -X230_bit2 -X230_bit3 -X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 -X232_bit_7 -X232_bit_6 -X232_bit_5 -X232_bit_4 -X232_bit_3 -X232_bit_2 -X232_bit_1 X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 -X233_bit_7 -X233_bit_6 -X233_bit_5 -X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 -X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 X234_bit_7 X234_bit_6 X234_bit_5 X234_bit_4 -X234_bit_3 -X234_bit_2 X234_bit_1 X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 -X235_bit_6 X235_bit_5 -X235_bit_4 -X235_bit_3 -X235_bit_2 -X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 -X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 X236_bit_7 X236_bit_6 -X236_bit_5 X236_bit_4 -X236_bit_3 X236_bit_2 X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 X237_bit_6 X237_bit_5 X237_bit_4 X237_bit_3 -X237_bit_2 -X237_bit_1 X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 -X241_bit_6 -X241_bit_5 -X241_bit_4 X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 X242_bit_1 X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 X243_bit_5 -X243_bit_4 -X243_bit_3 X243_bit_2 X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 X244_bit_6 X244_bit_5 -X244_bit_4 -X244_bit_3 X244_bit_2 X244_bit_1 X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 -X245_bit_7 -X245_bit_6 X245_bit_5 -X245_bit_4 X245_bit_3 -X245_bit_2 -X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 -X247_bit_7 X247_bit_6 -X247_bit_5 -X247_bit_4 X247_bit_3 -X247_bit_2 -X247_bit_1 X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 -X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 -X250_bit_5 -X250_bit_4 X250_bit_3 -X250_bit_2 -X250_bit_1 X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 X251_bit_7 X251_bit_6 X251_bit_5 -X251_bit_4 X251_bit_3 X251_bit_2 X251_bit_1 -X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 -X252_bit_6 -X252_bit_5 -X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 X253_bit_7 X253_bit_6 -X253_bit_5 X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 -X254_bit_6 X254_bit_5 -X254_bit_4 -X254_bit_3 X254_bit_2 -X254_bit_1 -X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 X255_bit_7 X255_bit_6 X255_bit_5 -X255_bit_4 X255_bit_3 -X255_bit_2 -X255_bit_1 -X255_bit0 X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 -X256_bit_7 -X256_bit_6 -X256_bit_5 -X256_bit_4 -X256_bit_3 -X256_bit_2 -X256_bit_1 -X256_bit0 X256_bit1 -X256_bit2 -X256_bit3 -X256_bit4 -X256_bit5 -X256_bit6 -X256_bit7 -X256_bit8 -X256_bit9 -X256_bit10 -X256_bit11 -X256_bit12 -X257_bit_7 -X257_bit_6 -X257_bit_5 -X257_bit_4 -X257_bit_3 -X257_bit_2 X257_bit_1 -X257_bit0 -X257_bit1 -X257_bit2 -X257_bit3 -X257_bit4 -X257_bit5 -X257_bit6 -X257_bit7 -X257_bit8 -X257_bit9 -X257_bit10 -X257_bit11 -X257_bit12 -X258_bit_7 -X258_bit_6 X258_bit_5 -X258_bit_4 -X258_bit_3 -X258_bit_2 X258_bit_1 X258_bit0 -X258_bit1 -X258_bit2 -X258_bit3 -X258_bit4 -X258_bit5 -X258_bit6 -X258_bit7 -X258_bit8 -X258_bit9 -X258_bit10 -X258_bit11 -X258_bit12 X259_bit_7 X259_bit_6 X259_bit_5 X259_bit_4 -X259_bit_3 X259_bit_2 X259_bit_1 -X259_bit0 X259_bit1 -X259_bit2 -X259_bit3 -X259_bit4 -X259_bit5 -X259_bit6 -X259_bit7 -X259_bit8 -X259_bit9 -X259_bit10 -X259_bit11 -X259_bit12 X260_bit_7 -X260_bit_6 X260_bit_5 -X260_bit_4 X260_bit_3 -X260_bit_2 X260_bit_1 X260_bit0 -X260_bit1 -X260_bit2 -X260_bit3 -X260_bit4 -X260_bit5 -X260_bit6 -X260_bit7 -X260_bit8 -X260_bit9 -X260_bit10 -X260_bit11 -X260_bit12 -X261_bit_7 -X261_bit_6 -X261_bit_5 -X261_bit_4 -X261_bit_3 -X261_bit_2 -X261_bit_1 -X261_bit0 -X261_bit1 -X261_bit2 -X261_bit3 -X261_bit4 -X261_bit5 -X261_bit6 -X261_bit7 -X261_bit8 -X261_bit9 -X261_bit10 -X261_bit11 -X261_bit12 -X262_bit_7 -X262_bit_6 -X262_bit_5 -X262_bit_4 -X262_bit_3 -X262_bit_2 -X262_bit_1 -X262_bit0 -X262_bit1 -X262_bit2 -X262_bit3 -X262_bit4 -X262_bit5 -X262_bit6 -X262_bit7 -X262_bit8 -X262_bit9 -X262_bit10 -X262_bit11 -X262_bit12 -X263_bit_7 -X263_bit_6 -X263_bit_5 -X263_bit_4 -X263_bit_3 -X263_bit_2 -X263_bit_1 -X263_bit0 -X263_bit1 -X263_bit2 -X263_bit3 -X263_bit4 -X263_bit5 -X263_bit6 -X263_bit7 -X263_bit8 -X263_bit9 -X263_bit10 -X263_bit11 -X263_bit12 X264_bit_7 X264_bit_6 X264_bit_5 X264_bit_4 -X264_bit_3 -X264_bit_2 X264_bit_1 X264_bit0 -X264_bit1 -X264_bit2 X264_bit3 -X264_bit4 -X264_bit5 -X264_bit6 -X264_bit7 -X264_bit8 -X264_bit9 -X264_bit10 -X264_bit11 -X264_bit12 -X265_bit_7 -X265_bit_6 -X265_bit_5 -X265_bit_4 -X265_bit_3 -X265_bit_2 -X265_bit_1 -X265_bit0 -X265_bit1 -X265_bit2 -X265_bit3 -X265_bit4 -X265_bit5 -X265_bit6 -X265_bit7 -X265_bit8 -X265_bit9 -X265_bit10 -X265_bit11 -X265_bit12 -X266_bit_7 -X266_bit_6 -X266_bit_5 -X266_bit_4 -X266_bit_3 -X266_bit_2 -X266_bit_1 -X266_bit0 -X266_bit1 -X266_bit2 -X266_bit3 -X266_bit4 -X266_bit5 -X266_bit6 -X266_bit7 -X266_bit8 -X266_bit9 -X266_bit10 -X266_bit11 -X266_bit12 -X267_bit_7 -X267_bit_6 -X267_bit_5 X267_bit_4 -X267_bit_3 -X267_bit_2 -X267_bit_1 X267_bit0 X267_bit1 -X267_bit2 -X267_bit3 -X267_bit4 -X267_bit5 -X267_bit6 -X267_bit7 -X267_bit8 -X267_bit9 -X267_bit10 -X267_bit11 -X267_bit12 X268_bit_7 -X268_bit_6 X268_bit_5 -X268_bit_4 -X268_bit_3 X268_bit_2 X268_bit_1 -X268_bit0 -X268_bit1 -X268_bit2 -X268_bit3 -X268_bit4 -X268_bit5 -X268_bit6 -X268_bit7 -X268_bit8 -X268_bit9 -X268_bit10 -X268_bit11 -X268_bit12 X269_bit_7 X269_bit_6 X269_bit_5 -X269_bit_4 -X269_bit_3 X269_bit_2 X269_bit_1 -X269_bit0 -X269_bit1 -X269_bit2 -X269_bit3 -X269_bit4 -X269_bit5 -X269_bit6 -X269_bit7 -X269_bit8 -X269_bit9 -X269_bit10 -X269_bit11 -X269_bit12 X270_bit_7 X270_bit_6 X270_bit_5 X270_bit_4 X270_bit_3 X270_bit_2 X270_bit_1 X270_bit0 -X270_bit1 -X270_bit2 -X270_bit3 -X270_bit4 -X270_bit5 -X270_bit6 -X270_bit7 -X270_bit8 -X270_bit9 -X270_bit10 -X270_bit11 -X270_bit12 X271_bit_7 X271_bit_6 X271_bit_5 X271_bit_4 X271_bit_3 X271_bit_2 X271_bit_1 -X271_bit0 -X271_bit1 -X271_bit2 -X271_bit3 -X271_bit4 -X271_bit5 -X271_bit6 -X271_bit7 -X271_bit8 -X271_bit9 -X271_bit10 -X271_bit11 -X271_bit12 X272_bit_7 -X272_bit_6 X272_bit_5 -X272_bit_4 X272_bit_3 -X272_bit_2 -X272_bit_1 -X272_bit0 -X272_bit1 -X272_bit2 -X272_bit3 -X272_bit4 -X272_bit5 -X272_bit6 -X272_bit7 -X272_bit8 -X272_bit9 -X272_bit10 -X272_bit11 -X272_bit12 -X273_bit_7 -X273_bit_6 -X273_bit_5 -X273_bit_4 -X273_bit_3 -X273_bit_2 -X273_bit_1 -X273_bit0 -X273_bit1 -X273_bit2 -X273_bit3 -X273_bit4 -X273_bit5 -X273_bit6 -X273_bit7 -X273_bit8 -X273_bit9 -X273_bit10 -X273_bit11 -X273_bit12 -X274_bit_7 -X274_bit_6 -X274_bit_5 -X274_bit_4 -X274_bit_3 -X274_bit_2 X274_bit_1 -X274_bit0 -X274_bit1 -X274_bit2 -X274_bit3 -X274_bit4 -X274_bit5 -X274_bit6 -X274_bit7 -X274_bit8 -X274_bit9 -X274_bit10 -X274_bit11 -X274_bit12 X275_bit_7 X275_bit_6 X275_bit_5 -X275_bit_4 X275_bit_3 X275_bit_2 X275_bit_1 -X275_bit0 X275_bit1 -X275_bit2 -X275_bit3 -X275_bit4 -X275_bit5 -X275_bit6 -X275_bit7 -X275_bit8 -X275_bit9 -X275_bit10 -X275_bit11 -X275_bit12 X276_bit_7 X276_bit_6 X276_bit_5 X276_bit_4 -X276_bit_3 X276_bit_2 X276_bit_1 X276_bit0 -X276_bit1 -X276_bit2 -X276_bit3 -X276_bit4 -X276_bit5 -X276_bit6 -X276_bit7 -X276_bit8 -X276_bit9 -X276_bit10 -X276_bit11 -X276_bit12 X277_bit_7 X277_bit_6 X277_bit_5 X277_bit_4 -X277_bit_3 -X277_bit_2 X277_bit_1 X277_bit0 X277_bit1 -X277_bit2 -X277_bit3 -X277_bit4 -X277_bit5 -X277_bit6 -X277_bit7 -X277_bit8 -X277_bit9 -X277_bit10 -X277_bit11 -X277_bit12 X278_bit_7 X278_bit_6 X278_bit_5 X278_bit_4 -X278_bit_3 -X278_bit_2 X278_bit_1 X278_bit0 X278_bit1 -X278_bit2 -X278_bit3 -X278_bit4 -X278_bit5 -X278_bit6 -X278_bit7 -X278_bit8 -X278_bit9 -X278_bit10 -X278_bit11 -X278_bit12 X279_bit_7 -X279_bit_6 -X279_bit_5 -X279_bit_4 -X279_bit_3 -X279_bit_2 -X279_bit_1 -X279_bit0 -X279_bit1 -X279_bit2 -X279_bit3 -X279_bit4 -X279_bit5 -X279_bit6 -X279_bit7 -X279_bit8 -X279_bit9 -X279_bit10 -X279_bit11 -X279_bit12 -X280_bit_7 -X280_bit_6 -X280_bit_5 -X280_bit_4 -X280_bit_3 -X280_bit_2 -X280_bit_1 -X280_bit0 -X280_bit1 -X280_bit2 -X280_bit3 -X280_bit4 -X280_bit5 -X280_bit6 -X280_bit7 -X280_bit8 -X280_bit9 -X280_bit10 -X280_bit11 -X280_bit12 -X281_bit_7 -X281_bit_6 -X281_bit_5 -X281_bit_4 -X281_bit_3 -X281_bit_2 -X281_bit_1 -X281_bit0 -X281_bit1 -X281_bit2 -X281_bit3 -X281_bit4 -X281_bit5 -X281_bit6 -X281_bit7 -X281_bit8 -X281_bit9 -X281_bit10 -X281_bit11 -X281_bit12 -X282_bit_7 -X282_bit_6 -X282_bit_5 -X282_bit_4 -X282_bit_3 -X282_bit_2 -X282_bit_1 -X282_bit0 X282_bit1 -X282_bit2 -X282_bit3 -X282_bit4 -X282_bit5 -X282_bit6 -X282_bit7 -X282_bit8 -X282_bit9 -X282_bit10 -X282_bit11 -X282_bit12 -X283_bit_7 -X283_bit_6 -X283_bit_5 -X283_bit_4 -X283_bit_3 -X283_bit_2 -X283_bit_1 -X283_bit0 -X283_bit1 -X283_bit2 -X283_bit3 -X283_bit4 -X283_bit5 -X283_bit6 -X283_bit7 -X283_bit8 -X283_bit9 -X283_bit10 -X283_bit11 -X283_bit12 -X284_bit_7 -X284_bit_6 -X284_bit_5 -X284_bit_4 -X284_bit_3 X284_bit_2 -X284_bit_1 -X284_bit0 X284_bit1 -X284_bit2 -X284_bit3 -X284_bit4 -X284_bit5 -X284_bit6 -X284_bit7 -X284_bit8 -X284_bit9 -X284_bit10 -X284_bit11 -X284_bit12 X285_bit_7 X285_bit_6 X285_bit_5 -X285_bit_4 -X285_bit_3 -X285_bit_2 -X285_bit_1 -X285_bit0 -X285_bit1 -X285_bit2 -X285_bit3 -X285_bit4 -X285_bit5 -X285_bit6 -X285_bit7 -X285_bit8 -X285_bit9 -X285_bit10 -X285_bit11 -X285_bit12 X286_bit_7 -X286_bit_6 X286_bit_5 -X286_bit_4 -X286_bit_3 X286_bit_2 -X286_bit_1 -X286_bit0 X286_bit1 -X286_bit2 -X286_bit3 -X286_bit4 -X286_bit5 -X286_bit6 -X286_bit7 -X286_bit8 -X286_bit9 -X286_bit10 -X286_bit11 -X286_bit12 X287_bit_7 X287_bit_6 -X287_bit_5 X287_bit_4 -X287_bit_3 X287_bit_2 X287_bit_1 X287_bit0 X287_bit1 -X287_bit2 X287_bit3 -X287_bit4 -X287_bit5 -X287_bit6 -X287_bit7 -X287_bit8 -X287_bit9 -X287_bit10 -X287_bit11 -X287_bit12 X288_bit_7 X288_bit_6 X288_bit_5 X288_bit_4 -X288_bit_3 X288_bit_2 X288_bit_1 X288_bit0 X288_bit1 -X288_bit2 -X288_bit3 -X288_bit4 -X288_bit5 -X288_bit6 -X288_bit7 -X288_bit8 -X288_bit9 -X288_bit10 -X288_bit11 -X288_bit12 Y0_bit0 -Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 Y6_bit0 Y7_bit0 Y8_bit0 Y9_bit0 -Y10_bit0 Y11_bit0 Y12_bit0 -Y13_bit0 -Y14_bit0 -Y15_bit0 Y16_bit0 -Y17_bit0 Y18_bit0 Y19_bit0 Y20_bit0 -Y21_bit0 -Y22_bit0 -Y23_bit0 -Y24_bit0 Y25_bit0 Y26_bit0 Y27_bit0 Y28_bit0 -Y29_bit0 Y30_bit0 Y31_bit0 -Y32_bit0 -Y33_bit0 Y34_bit0 -Y35_bit0 Y36_bit0 Y37_bit0 Y38_bit0 Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 Y43_bit0 -Y44_bit0 Y45_bit0 Y46_bit0 Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 Y51_bit0 Y52_bit0 -Y53_bit0 Y54_bit0 Y55_bit0 -Y56_bit0 Y57_bit0 -Y58_bit0 Y59_bit0 Y60_bit0 Y61_bit0 Y62_bit0 Y63_bit0 Y64_bit0 Y65_bit0 Y66_bit0 Y67_bit0 Y68_bit0 -Y69_bit0 -Y70_bit0 Y71_bit0 Y72_bit0 -Y73_bit0 Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 -Y79_bit0 Y80_bit0 Y81_bit0 Y82_bit0 Y83_bit0 Y84_bit0 Y85_bit0 -Y86_bit0 -Y87_bit0 Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 Y95_bit0 Y96_bit0 Y97_bit0 Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 Y102_bit0 Y103_bit0 Y104_bit0 -Y105_bit0 Y106_bit0 Y107_bit0 Y108_bit0 Y109_bit0 Y110_bit0 Y111_bit0 Y112_bit0 -Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 Y118_bit0 Y119_bit0 -Y120_bit0 -Y121_bit0 Y122_bit0 -Y123_bit0 Y124_bit0 Y125_bit0 Y126_bit0 Y127_bit0 Y128_bit0 -Y129_bit0 -Y130_bit0 Y131_bit0 Y132_bit0 Y133_bit0 Y134_bit0 Y135_bit0 Y136_bit0 -Y137_bit0 Y138_bit0 Y139_bit0 Y140_bit0 -Y141_bit0 Y142_bit0 -Y143_bit0 -Y144_bit0 Y145_bit0 Y146_bit0 -Y147_bit0 Y148_bit0 Y149_bit0 Y150_bit0 Y151_bit0 Y152_bit0 Y153_bit0 Y154_bit0 Y155_bit0 -Y156_bit0 Y157_bit0 Y158_bit0 -Y159_bit0 Y160_bit0 Y161_bit0 Y162_bit0 -Y163_bit0 Y164_bit0 Y165_bit0 -Y166_bit0 -Y167_bit0 Y168_bit0 -Y169_bit0 Y170_bit0 Y171_bit0 -Y172_bit0 Y173_bit0 Y174_bit0 Y175_bit0 Y176_bit0 Y177_bit0 -Y178_bit0 -Y179_bit0 Y180_bit0 -Y181_bit0 Y182_bit0 Y183_bit0 Y184_bit0 -Y185_bit0 Y186_bit0 Y187_bit0 Y188_bit0 -Y189_bit0 Y190_bit0 Y191_bit0 Y192_bit0 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 1.00 0.95 2/54 18715
Raw data (stat): 18715 (runsolver) R 18714 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544555478 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.94 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 34962 0 0 0 918 79 0 0 25 0 1 0 544555478 150515712 32264 4294967295 134512640 134672761 3221224528 3221173488 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36747 32264 603 41 0 36706 0
vsize: 146988
[startup+20.0016 s]
Raw data (loadavg): 0.95 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56331 0 0 0 1868 130 0 0 25 0 1 0 544555478 251617280 53633 4294967295 134512640 134672761 3221224528 3221223676 1074733101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61430 53633 603 41 0 61389 0
vsize: 245720
[startup+30.0021 s]
Raw data (loadavg): 0.96 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56360 0 0 0 2867 130 0 0 25 0 1 0 544555478 251752448 53662 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61463 53662 603 41 0 61422 0
vsize: 245852
[startup+40.0017 s]
Raw data (loadavg): 0.96 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56400 0 0 0 3866 131 0 0 25 0 1 0 544555478 252018688 53702 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61528 53702 603 41 0 61487 0
vsize: 246112
[startup+50.0028 s]
Raw data (loadavg): 0.97 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56436 0 0 0 4867 131 0 0 25 0 1 0 544555478 252018688 53738 4294967295 134512640 134672761 3221224528 3221223696 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61528 53738 603 41 0 61487 0
vsize: 246112
[startup+60.0026 s]
Raw data (loadavg): 0.97 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56539 0 0 0 5866 131 0 0 25 0 1 0 544555478 252289024 53841 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61594 53841 603 41 0 61553 0
vsize: 246376
[startup+70.0031 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56596 0 0 0 6866 132 0 0 25 0 1 0 544555478 252559360 53898 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61660 53898 603 41 0 61619 0
vsize: 246640
[startup+80.0033 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56624 0 0 0 7866 132 0 0 25 0 1 0 544555478 252694528 53926 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61693 53926 603 41 0 61652 0
vsize: 246772
[startup+90.0031 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56669 0 0 0 8866 132 0 0 25 0 1 0 544555478 252829696 53971 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61726 53971 603 41 0 61685 0
vsize: 246904
[startup+100.004 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56722 0 0 0 9866 132 0 0 25 0 1 0 544555478 253087744 54024 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61789 54024 603 41 0 61748 0
vsize: 247156
[startup+110.004 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56825 0 0 0 10866 133 0 0 25 0 1 0 544555478 253493248 54127 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61888 54127 603 41 0 61847 0
vsize: 247552
[startup+120.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 56933 0 0 0 11866 133 0 0 25 0 1 0 544555478 253898752 54235 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61987 54235 603 41 0 61946 0
vsize: 247948
[startup+130.004 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57087 0 0 0 12865 133 0 0 25 0 1 0 544555478 254566400 54389 4294967295 134512640 134672761 3221224528 3221223696 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62150 54389 603 41 0 62109 0
vsize: 248600
[startup+140.004 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57187 0 0 0 13865 134 0 0 25 0 1 0 544555478 255098880 54489 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62280 54489 603 41 0 62239 0
vsize: 249120
[startup+150.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57277 0 0 0 14865 134 0 0 25 0 1 0 544555478 255496192 54579 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62377 54579 603 41 0 62336 0
vsize: 249508
[startup+160.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57441 0 0 0 15865 134 0 0 25 0 1 0 544555478 256172032 54743 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62542 54743 603 41 0 62501 0
vsize: 250168
[startup+170.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57562 0 0 0 16865 134 0 0 25 0 1 0 544555478 256577536 54864 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62641 54864 603 41 0 62600 0
vsize: 250564
[startup+180.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57768 0 0 0 17865 135 0 0 25 0 1 0 544555478 257376256 55070 4294967295 134512640 134672761 3221224528 3221223632 134559985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62836 55070 603 41 0 62795 0
vsize: 251344
[startup+190.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 57855 0 0 0 18865 135 0 0 25 0 1 0 544555478 257777664 55157 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62934 55157 603 41 0 62893 0
vsize: 251736
[startup+200.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58033 0 0 0 19864 136 0 0 25 0 1 0 544555478 258048000 55335 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63000 55335 603 41 0 62959 0
vsize: 252000
[startup+210.005 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58287 0 0 0 20864 136 0 0 25 0 1 0 544555478 259125248 55589 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63263 55589 603 41 0 63222 0
vsize: 253052
[startup+220.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58479 0 0 0 21863 137 0 0 25 0 1 0 544555478 259936256 55781 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63461 55781 603 41 0 63420 0
vsize: 253844
[startup+230.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58518 0 0 0 22863 137 0 0 25 0 1 0 544555478 260067328 55820 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63493 55820 603 41 0 63452 0
vsize: 253972
[startup+240.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58605 0 0 0 23863 137 0 0 25 0 1 0 544555478 260333568 55907 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63558 55907 603 41 0 63517 0
vsize: 254232
[startup+250.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58687 0 0 0 24862 138 0 0 25 0 1 0 544555478 260739072 55989 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63657 55989 603 41 0 63616 0
vsize: 254628
[startup+260.006 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18715
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58824 0 0 0 25862 139 0 0 25 0 1 0 544555478 261275648 56126 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63788 56126 603 41 0 63747 0
vsize: 255152
[startup+270.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58952 0 0 0 26862 139 0 0 25 0 1 0 544555478 262098944 56254 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63989 56254 603 41 0 63948 0
vsize: 255956
[startup+280.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 58987 0 0 0 27862 139 0 0 25 0 1 0 544555478 262234112 56289 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64022 56289 603 41 0 63981 0
vsize: 256088
[startup+290.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59049 0 0 0 28862 139 0 0 25 0 1 0 544555478 262369280 56351 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64055 56351 603 41 0 64014 0
vsize: 256220
[startup+300.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59131 0 0 0 29862 140 0 0 25 0 1 0 544555478 262770688 56433 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64153 56433 603 41 0 64112 0
vsize: 256612
[startup+310.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59214 0 0 0 30862 140 0 0 25 0 1 0 544555478 263041024 56516 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64219 56516 603 41 0 64178 0
vsize: 256876
[startup+320.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59284 0 0 0 31862 140 0 0 25 0 1 0 544555478 263307264 56586 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64284 56586 603 41 0 64243 0
vsize: 257136
[startup+330.008 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59353 0 0 0 32862 140 0 0 25 0 1 0 544555478 263577600 56655 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64350 56655 603 41 0 64309 0
vsize: 257400
[startup+340.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59458 0 0 0 33862 141 0 0 25 0 1 0 544555478 264105984 56760 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64479 56760 603 41 0 64438 0
vsize: 257916
[startup+350.115 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59542 0 0 0 34872 141 0 0 25 0 1 0 544555478 264376320 56844 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64545 56844 603 41 0 64504 0
vsize: 258180
[startup+360.115 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59607 0 0 0 35872 141 0 0 25 0 1 0 544555478 264638464 56909 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64609 56909 603 41 0 64568 0
vsize: 258436
[startup+370.115 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59688 0 0 0 36872 142 0 0 25 0 1 0 544555478 264908800 56990 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64675 56990 603 41 0 64634 0
vsize: 258700
[startup+380.115 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59802 0 0 0 37871 142 0 0 25 0 1 0 544555478 265441280 57104 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64805 57104 603 41 0 64764 0
vsize: 259220
[startup+390.115 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 59907 0 0 0 38871 142 0 0 25 0 1 0 544555478 265846784 57209 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64904 57209 603 41 0 64863 0
vsize: 259616
[startup+400.116 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 60004 0 0 0 39871 142 0 0 25 0 1 0 544555478 266248192 57306 4294967295 134512640 134672761 3221224528 3221223728 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65002 57306 603 41 0 64961 0
vsize: 260008
[startup+410.116 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 60060 0 0 0 40871 143 0 0 25 0 1 0 544555478 266518528 57362 4294967295 134512640 134672761 3221224528 3221223732 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65068 57362 603 41 0 65027 0
vsize: 260272
[startup+420.116 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 60079 0 0 0 41872 143 0 0 25 0 1 0 544555478 266518528 57381 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65068 57381 603 41 0 65027 0
vsize: 260272
[startup+430.116 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 60193 0 0 0 42871 143 0 0 25 0 1 0 544555478 266924032 57495 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65167 57495 603 41 0 65126 0
vsize: 260668
[startup+440.116 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 60508 0 0 0 43870 144 0 0 25 0 1 0 544555478 267460608 57810 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65298 57810 603 41 0 65257 0
vsize: 261192
[startup+450.117 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61349 0 0 0 44869 146 0 0 25 0 1 0 544555478 270995456 58511 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66161 58511 603 41 0 66120 0
vsize: 264644
[startup+460.117 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61350 0 0 0 45869 146 0 0 25 0 1 0 544555478 270995456 58512 4294967295 134512640 134672761 3221224528 3221223712 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66161 58512 603 41 0 66120 0
vsize: 264644
[startup+470.118 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61355 0 0 0 46869 146 0 0 25 0 1 0 544555478 271130624 58517 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66194 58517 603 41 0 66153 0
vsize: 264776
[startup+480.117 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61377 0 0 0 47869 146 0 0 25 0 1 0 544555478 271130624 58539 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66194 58539 603 41 0 66153 0
vsize: 264776
[startup+490.117 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61402 0 0 0 48869 146 0 0 25 0 1 0 544555478 271265792 58564 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66227 58564 603 41 0 66186 0
vsize: 264908
[startup+500.118 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61425 0 0 0 49869 146 0 0 25 0 1 0 544555478 271396864 58587 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66259 58587 603 41 0 66218 0
vsize: 265036
[startup+510.118 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61451 0 0 0 50869 146 0 0 25 0 1 0 544555478 271396864 58613 4294967295 134512640 134672761 3221224528 3221223664 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66259 58613 603 41 0 66218 0
vsize: 265036
[startup+520.118 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61493 0 0 0 51869 146 0 0 25 0 1 0 544555478 271663104 58655 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66324 58655 603 41 0 66283 0
vsize: 265296
[startup+530.119 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61566 0 0 0 52869 147 0 0 25 0 1 0 544555478 271933440 58728 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66390 58728 603 41 0 66349 0
vsize: 265560
[startup+540.118 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61681 0 0 0 53869 147 0 0 25 0 1 0 544555478 272338944 58843 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66489 58843 603 41 0 66448 0
vsize: 265956
[startup+550.119 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 61905 0 0 0 54869 148 0 0 25 0 1 0 544555478 273272832 59067 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66717 59067 603 41 0 66676 0
vsize: 266868
[startup+560.119 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62053 0 0 0 55869 148 0 0 25 0 1 0 544555478 273944576 59215 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66881 59215 603 41 0 66840 0
vsize: 267524
[startup+570.12 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62169 0 0 0 56869 148 0 0 25 0 1 0 544555478 274350080 59331 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66980 59331 603 41 0 66939 0
vsize: 267920
[startup+580.12 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62238 0 0 0 57869 148 0 0 25 0 1 0 544555478 274620416 59400 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67046 59400 603 41 0 67005 0
vsize: 268184
[startup+590.12 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62339 0 0 0 58868 149 0 0 25 0 1 0 544555478 275021824 59501 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67144 59501 603 41 0 67103 0
vsize: 268576
[startup+600.12 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62402 0 0 0 59868 149 0 0 25 0 1 0 544555478 275288064 59564 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67209 59564 603 41 0 67168 0
vsize: 268836
[startup+610.121 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62571 0 0 0 60868 150 0 0 25 0 1 0 544555478 276488192 59733 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67502 59733 603 41 0 67461 0
vsize: 270008
[startup+620.121 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 62730 0 0 0 61868 150 0 0 25 0 1 0 544555478 277159936 59892 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67666 59892 603 41 0 67625 0
vsize: 270664
[startup+630.121 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63009 0 0 0 62867 151 0 0 25 0 1 0 544555478 278237184 60171 4294967295 134512640 134672761 3221224528 3221223468 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67929 60171 603 41 0 67888 0
vsize: 271716
[startup+640.121 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63156 0 0 0 63866 152 0 0 25 0 1 0 544555478 278777856 60318 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68061 60318 603 41 0 68020 0
vsize: 272244
[startup+650.122 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63180 0 0 0 64866 152 0 0 25 0 1 0 544555478 278913024 60342 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68094 60342 603 41 0 68053 0
vsize: 272376
[startup+660.121 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63193 0 0 0 65867 152 0 0 25 0 1 0 544555478 278913024 60355 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68094 60355 603 41 0 68053 0
vsize: 272376
[startup+670.122 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63312 0 0 0 66867 152 0 0 25 0 1 0 544555478 279441408 60474 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68223 60474 603 41 0 68182 0
vsize: 272892
[startup+680.123 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63403 0 0 0 67867 152 0 0 25 0 1 0 544555478 279842816 60565 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68321 60565 603 41 0 68280 0
vsize: 273284
[startup+690.123 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63456 0 0 0 68867 152 0 0 25 0 1 0 544555478 279977984 60618 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68354 60618 603 41 0 68313 0
vsize: 273416
[startup+700.124 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63567 0 0 0 69866 153 0 0 25 0 1 0 544555478 280473600 60729 4294967295 134512640 134672761 3221224528 3221223728 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68475 60729 603 41 0 68434 0
vsize: 273900
[startup+710.125 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63631 0 0 0 70866 153 0 0 25 0 1 0 544555478 280739840 60793 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68540 60793 603 41 0 68499 0
vsize: 274160
[startup+720.125 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63710 0 0 0 71866 154 0 0 25 0 1 0 544555478 281010176 60872 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68606 60872 603 41 0 68565 0
vsize: 274424
[startup+730.125 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63770 0 0 0 72866 154 0 0 25 0 1 0 544555478 281280512 60932 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68672 60932 603 41 0 68631 0
vsize: 274688
[startup+740.125 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63797 0 0 0 73866 154 0 0 25 0 1 0 544555478 281411584 60959 4294967295 134512640 134672761 3221224528 3221223664 134560625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68704 60959 603 41 0 68663 0
vsize: 274816
[startup+750.126 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63875 0 0 0 74866 154 0 0 25 0 1 0 544555478 281681920 61037 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68770 61037 603 41 0 68729 0
vsize: 275080
[startup+760.126 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63923 0 0 0 75866 154 0 0 25 0 1 0 544555478 281952256 61085 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68836 61085 603 41 0 68795 0
vsize: 275344
[startup+770.126 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 63985 0 0 0 76865 155 0 0 25 0 1 0 544555478 282087424 61147 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68869 61147 603 41 0 68828 0
vsize: 275476
[startup+780.127 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64034 0 0 0 77866 155 0 0 25 0 1 0 544555478 282345472 61196 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68932 61196 603 41 0 68891 0
vsize: 275728
[startup+790.127 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64074 0 0 0 78866 155 0 0 25 0 1 0 544555478 282476544 61236 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68964 61236 603 41 0 68923 0
vsize: 275856
[startup+800.128 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64127 0 0 0 79866 155 0 0 25 0 1 0 544555478 282746880 61289 4294967295 134512640 134672761 3221224528 3221223728 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69030 61289 603 41 0 68989 0
vsize: 276120
[startup+810.128 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64158 0 0 0 80866 155 0 0 25 0 1 0 544555478 282746880 61320 4294967295 134512640 134672761 3221224528 3221223664 134560686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69030 61320 603 41 0 68989 0
vsize: 276120
[startup+820.129 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64195 0 0 0 81866 155 0 0 25 0 1 0 544555478 283017216 61357 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69096 61357 603 41 0 69055 0
vsize: 276384
[startup+830.13 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64224 0 0 0 82866 155 0 0 25 0 1 0 544555478 283017216 61386 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69096 61386 603 41 0 69055 0
vsize: 276384
[startup+840.129 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64288 0 0 0 83866 155 0 0 25 0 1 0 544555478 283287552 61450 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69162 61450 603 41 0 69121 0
vsize: 276648
[startup+850.13 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64378 0 0 0 84866 156 0 0 25 0 1 0 544555478 283693056 61540 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69261 61540 603 41 0 69220 0
vsize: 277044
[startup+860.13 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64433 0 0 0 85866 156 0 0 25 0 1 0 544555478 283963392 61595 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69327 61595 603 41 0 69286 0
vsize: 277308
[startup+870.13 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64485 0 0 0 86866 156 0 0 25 0 1 0 544555478 284094464 61647 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69359 61647 603 41 0 69318 0
vsize: 277436
[startup+880.131 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64568 0 0 0 87866 157 0 0 25 0 1 0 544555478 284491776 61730 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69456 61730 603 41 0 69415 0
vsize: 277824
[startup+890.131 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64663 0 0 0 88866 157 0 0 25 0 1 0 544555478 284762112 61825 4294967295 134512640 134672761 3221224528 3221223664 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69522 61825 603 41 0 69481 0
vsize: 278088
[startup+900.132 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64755 0 0 0 89866 157 0 0 25 0 1 0 544555478 285163520 61917 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69620 61917 603 41 0 69579 0
vsize: 278480
[startup+910.132 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64885 0 0 0 90865 158 0 0 25 0 1 0 544555478 285700096 62047 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69751 62047 603 41 0 69710 0
vsize: 279004
[startup+920.134 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64905 0 0 0 91865 158 0 0 25 0 1 0 544555478 285831168 62067 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69783 62067 603 41 0 69742 0
vsize: 279132
[startup+930.134 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 64941 0 0 0 92865 158 0 0 25 0 1 0 544555478 285962240 62103 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69815 62103 603 41 0 69774 0
vsize: 279260
[startup+940.134 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65009 0 0 0 93865 158 0 0 25 0 1 0 544555478 286302208 62171 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69898 62171 603 41 0 69857 0
vsize: 279592
[startup+950.134 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65048 0 0 0 94865 158 0 0 25 0 1 0 544555478 286429184 62210 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69929 62210 603 41 0 69888 0
vsize: 279716
[startup+960.135 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65057 0 0 0 95865 159 0 0 25 0 1 0 544555478 286429184 62219 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69929 62219 603 41 0 69888 0
vsize: 279716
[startup+970.136 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65082 0 0 0 96865 159 0 0 25 0 1 0 544555478 286564352 62244 4294967295 134512640 134672761 3221224528 3221223696 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69962 62244 603 41 0 69921 0
vsize: 279848
[startup+980.136 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65309 0 0 0 97865 159 0 0 25 0 1 0 544555478 287506432 62471 4294967295 134512640 134672761 3221224528 3221223632 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70192 62471 603 41 0 70151 0
vsize: 280768
[startup+990.135 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65667 0 0 0 98864 160 0 0 25 0 1 0 544555478 288993280 62829 4294967295 134512640 134672761 3221224528 3221223632 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70555 62829 603 41 0 70514 0
vsize: 282220
[startup+1000.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 65995 0 0 0 99863 161 0 0 25 0 1 0 544555478 290336768 63157 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70883 63157 603 41 0 70842 0
vsize: 283532
[startup+1010.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66142 0 0 0 100863 162 0 0 25 0 1 0 544555478 290869248 63304 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71013 63304 603 41 0 70972 0
vsize: 284052
[startup+1020.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66209 0 0 0 101863 162 0 0 25 0 1 0 544555478 291139584 63371 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71079 63371 603 41 0 71038 0
vsize: 284316
[startup+1030.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66290 0 0 0 102863 162 0 0 25 0 1 0 544555478 291409920 63452 4294967295 134512640 134672761 3221224528 3221223632 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71145 63452 603 41 0 71104 0
vsize: 284580
[startup+1040.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66499 0 0 0 103862 163 0 0 25 0 1 0 544555478 292352000 63661 4294967295 134512640 134672761 3221224528 3221223632 134560019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71375 63661 603 41 0 71334 0
vsize: 285500
[startup+1050.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66694 0 0 0 104862 164 0 0 25 0 1 0 544555478 293163008 63856 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71573 63856 603 41 0 71532 0
vsize: 286292
[startup+1060.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66800 0 0 0 105861 164 0 0 25 0 1 0 544555478 293568512 63962 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71672 63962 603 41 0 71631 0
vsize: 286688
[startup+1070.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66834 0 0 0 106862 164 0 0 25 0 1 0 544555478 293703680 63996 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71705 63996 603 41 0 71664 0
vsize: 286820
[startup+1080.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66862 0 0 0 107862 165 0 0 25 0 1 0 544555478 293703680 64024 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71705 64024 603 41 0 71664 0
vsize: 286820
[startup+1090.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66876 0 0 0 108861 165 0 0 25 0 1 0 544555478 293838848 64038 4294967295 134512640 134672761 3221224528 3221223688 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71738 64038 603 41 0 71697 0
vsize: 286952
[startup+1100.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 66892 0 0 0 109862 165 0 0 25 0 1 0 544555478 293838848 64054 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71738 64054 603 41 0 71697 0
vsize: 286952
[startup+1110.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 67105 0 0 0 110861 166 0 0 25 0 1 0 544555478 294780928 64267 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71968 64267 603 41 0 71927 0
vsize: 287872
[startup+1120.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 67342 0 0 0 111861 166 0 0 25 0 1 0 544555478 295714816 64504 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72196 64504 603 41 0 72155 0
vsize: 288784
[startup+1130.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 67777 0 0 0 112859 168 0 0 25 0 1 0 544555478 297467904 64939 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72624 64939 603 41 0 72583 0
vsize: 290496
[startup+1140.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68133 0 0 0 113858 169 0 0 25 0 1 0 544555478 298946560 65295 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72985 65295 603 41 0 72944 0
vsize: 291940
[startup+1150.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68378 0 0 0 114858 170 0 0 25 0 1 0 544555478 299888640 65540 4294967295 134512640 134672761 3221224528 3221223632 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73215 65540 603 41 0 73174 0
vsize: 292860
[startup+1160.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68460 0 0 0 115857 170 0 0 25 0 1 0 544555478 300294144 65622 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73314 65622 603 41 0 73273 0
vsize: 293256
[startup+1170.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68491 0 0 0 116857 170 0 0 25 0 1 0 544555478 300294144 65653 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73314 65653 603 41 0 73273 0
vsize: 293256
[startup+1180.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68495 0 0 0 117857 170 0 0 25 0 1 0 544555478 300429312 65657 4294967295 134512640 134672761 3221224528 3221223728 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73347 65657 603 41 0 73306 0
vsize: 293388
[startup+1190.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68553 0 0 0 118857 170 0 0 25 0 1 0 544555478 300564480 65715 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73380 65715 603 41 0 73339 0
vsize: 293520
[startup+1200.14 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 18717
Raw data (stat): 18715 (minisat+) R 18714 18865 18864 0 -1 0 68646 0 0 0 119857 171 0 0 25 0 1 0 544555478 300969984 65808 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73479 65808 603 41 0 73438 0
vsize: 293916
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.29 s]
Raw data (loadavg): 0.99 1.00 0.95 1/54 18717
Raw data (stat): 18715 (minisat+) Z 18714 18865 18864 0 -1 12 68649 0 0 0 119858 184 0 0 25 0 1 0 544555478 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.29
CPU time (s): 1200.43
CPU user time (s): 1198.59
CPU system time (s): 1.84372
CPU usage (%): 100.012
Max. virtual memory (Kb): 293916
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####