PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 11:31:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19318 boxname=wulflinc29 idbench=1486 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9ccd6fd38eec7ec6eedca3a615a280ba  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran16x16.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran16x16.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-ran16x16.opb
IDLAUNCH: 19318
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        741160 kB
Buffers:          4312 kB
Cached:         265804 kB
SwapCached:        524 kB
Active:          56824 kB
Inactive:       215280 kB
HighTotal:      131008 kB
HighFree:         2324 kB
LowTotal:       903652 kB
LowFree:        738836 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15848 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:51:53 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 19318 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 320 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 318]---> Adder-cost: 332   maxlim: 41712   bits: 16/16
c ---[ 316]---> Adder-cost: 332   maxlim: 41456   bits: 16/16
c ---[ 314]---> Adder-cost: 332   maxlim: 42096   bits: 16/16
c ---[ 312]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 310]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 308]---> Adder-cost: 316   maxlim: 24432   bits: 15/15
c ---[ 306]---> Adder-cost: 336   maxlim: 51952   bits: 16/16
c ---[ 304]---> Adder-cost: 292   maxlim: 13040   bits: 14/14
c ---[ 302]---> Adder-cost: 316   maxlim: 24816   bits: 15/15
c ---[ 300]---> Adder-cost: 268   maxlim: 7280   bits: 13/13
c ---[ 298]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 296]---> Adder-cost: 336   maxlim: 49904   bits: 16/16
c ---[ 294]---> Adder-cost: 316   maxlim: 24944   bits: 15/15
c ---[ 292]---> Adder-cost: 332   maxlim: 42352   bits: 16/16
c ---[ 290]---> Adder-cost: 316   maxlim: 24176   bits: 15/15
c ---[ 288]---> Adder-cost: 332   maxlim: 42224   bits: 16/16
c ---[ 286]---> Adder-cost: 328   maxlim: 27760   bits: 15/15
c ---[ 284]---> Adder-cost: 344   maxlim: 44528   bits: 16/16
c ---[ 282]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 280]---> Adder-cost: 350   maxlim: 52208   bits: 16/16
c ---[ 278]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 276]---> Adder-cost: 240   maxlim: 3952   bits: 12/12
c ---[ 274]---> Adder-cost: 344   maxlim: 43760   bits: 16/16
c ---[ 272]---> Adder-cost: 344   maxlim: 45424   bits: 16/16
c ---[ 270]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 268]---> Adder-cost: 350   maxlim: 53616   bits: 16/16
c ---[ 266]---> Adder-cost: 270   maxlim: 7920   bits: 13/13
c ---[ 264]---> Adder-cost: 344   maxlim: 44784   bits: 16/16
c ---[ 262]---> Adder-cost: 350   maxlim: 54640   bits: 16/16
c ---[ 260]---> Adder-cost: 328   maxlim: 28144   bits: 15/15
c ---[ 258]---> Adder-cost: 328   maxlim: 28016   bits: 15/15
c ---[ 256]---> Adder-cost: 344   maxlim: 45552   bits: 16/16
c ---[ 255]---> BDD-cost:   15
c ---[ 254]---> BDD-cost:   16
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   15
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:   12
c ---[ 248]---> BDD-cost:   15
c ---[ 247]---> BDD-cost:   15
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:   15
c ---[ 244]---> BDD-cost:   15
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:   16
c ---[ 241]---> BDD-cost:   15
c ---[ 240]---> BDD-cost:   15
c ---[ 239]---> BDD-cost:   15
c ---[ 238]---> BDD-cost:   17
c ---[ 237]---> BDD-cost:   10
c ---[ 236]---> BDD-cost:   17
c ---[ 235]---> BDD-cost:   10
c ---[ 234]---> BDD-cost:   17
c ---[ 233]---> BDD-cost:   17
c ---[ 232]---> BDD-cost:   12
c ---[ 231]---> BDD-cost:   17
c ---[ 230]---> BDD-cost:   15
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:   17
c ---[ 226]---> BDD-cost:   17
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:   17
c ---[ 223]---> BDD-cost:   17
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:   15
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:   10
c ---[ 218]---> BDD-cost:   15
c ---[ 217]---> BDD-cost:   10
c ---[ 216]---> BDD-cost:   15
c ---[ 215]---> BDD-cost:   15
c ---[ 214]---> BDD-cost:   12
c ---[ 213]---> BDD-cost:   15
c ---[ 212]---> BDD-cost:   15
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:   15
c ---[ 209]---> BDD-cost:   16
c ---[ 208]---> BDD-cost:   15
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:   15
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:   15
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:   10
c ---[ 201]---> BDD-cost:   16
c ---[ 200]---> BDD-cost:   10
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:   17
c ---[ 197]---> BDD-cost:   16
c ---[ 196]---> BDD-cost:   12
c ---[ 195]---> BDD-cost:   15
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:   17
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:   16
c ---[ 188]---> BDD-cost:   17
c ---[ 187]---> BDD-cost:   15
c ---[ 186]---> BDD-cost:   15
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   17
c ---[ 182]---> BDD-cost:   10
c ---[ 181]---> BDD-cost:   17
c ---[ 180]---> BDD-cost:   17
c ---[ 179]---> BDD-cost:   12
c ---[ 178]---> BDD-cost:   15
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   14
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:   17
c ---[ 173]---> BDD-cost:   17
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:   17
c ---[ 170]---> BDD-cost:   17
c ---[ 169]---> BDD-cost:   15
c ---[ 168]---> BDD-cost:   14
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   18
c ---[ 165]---> BDD-cost:   10
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:   18
c ---[ 161]---> BDD-cost:   12
c ---[ 160]---> BDD-cost:   15
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:   18
c ---[ 156]---> BDD-cost:   17
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:   14
c ---[ 153]---> BDD-cost:   16
c ---[ 152]---> BDD-cost:   17
c ---[ 151]---> BDD-cost:   12
c ---[ 150]---> BDD-cost:   12
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:   12
c ---[ 147]---> BDD-cost:   10
c ---[ 146]---> BDD-cost:   12
c ---[ 145]---> BDD-cost:   12
c ---[ 144]---> BDD-cost:   12
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:   12
c ---[ 140]---> BDD-cost:   12
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:   12
c ---[ 137]---> BDD-cost:   12
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:   12
c ---[ 134]---> BDD-cost:   12
c ---[ 133]---> BDD-cost:   15
c ---[ 132]---> BDD-cost:   15
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:   10
c ---[ 129]---> BDD-cost:   15
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:   12
c ---[ 124]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   15
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   15
c ---[ 120]---> BDD-cost:   14
c ---[ 119]---> BDD-cost:   15
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:   15
c ---[ 116]---> BDD-cost:   15
c ---[ 115]---> BDD-cost:   15
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   18
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   16
c ---[ 109]---> BDD-cost:   12
c ---[ 108]---> BDD-cost:   18
c ---[ 107]---> BDD-cost:   12
c ---[ 106]---> BDD-cost:   15
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:   18
c ---[ 102]---> BDD-cost:   17
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:   16
c ---[  99]---> BDD-cost:   17
c ---[  98]---> BDD-cost:   15
c ---[  97]---> BDD-cost:   12
c ---[  96]---> BDD-cost:   12
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   12
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   12
c ---[  91]---> BDD-cost:   12
c ---[  90]---> BDD-cost:   12
c ---[  89]---> BDD-cost:   12
c ---[  88]---> BDD-cost:   12
c ---[  87]---> BDD-cost:   13
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:   12
c ---[  84]---> BDD-cost:   12
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:   12
c ---[  81]---> BDD-cost:   12
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:   16
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:   14
c ---[  72]---> BDD-cost:   14
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   14
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   12
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   15
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:   14
c ---[  60]---> BDD-cost:   14
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:   14
c ---[  56]---> BDD-cost:   11
c ---[  55]---> BDD-cost:   11
c ---[  54]---> BDD-cost:   16
c ---[  53]---> BDD-cost:   10
c ---[  52]---> BDD-cost:   11
c ---[  51]---> BDD-cost:   10
c ---[  50]---> BDD-cost:   11
c ---[  49]---> BDD-cost:   11
c ---[  48]---> BDD-cost:   11
c ---[  47]---> BDD-cost:   11
c ---[  46]---> BDD-cost:   11
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:   11
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:   11
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:   11
c ---[  39]---> BDD-cost:   11
c ---[  38]---> BDD-cost:   15
c ---[  37]---> BDD-cost:   16
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:   16
c ---[  32]---> BDD-cost:   12
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:   12
c ---[  29]---> BDD-cost:   15
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:   16
c ---[  25]---> BDD-cost:   17
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:   16
c ---[  22]---> BDD-cost:   17
c ---[  21]---> BDD-cost:   15
c ---[  20]---> BDD-cost:   15
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   19
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   16
c ---[  14]---> BDD-cost:   19
c ---[  13]---> BDD-cost:   12
c ---[  12]---> BDD-cost:   15
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   13
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:   18
c ---[   7]---> BDD-cost:   17
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   15
c ---[   1]---> BDD-cost:   10
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   74528   259510 |   24842       0        0     nan |  0.000 % |
c |       100 |   74502   259422 |   27326      98      361     3.7 | 21.038 % |
c |       250 |   74502   259422 |   30058     248      829     3.3 | 21.038 % |
c |       475 |   74502   259422 |   33064     473     1523     3.2 | 21.038 % |
c |       812 |   74428   259178 |   36371     802     2627     3.3 | 21.113 % |
c |      1318 |   74161   258277 |   40008    1278     4178     3.3 | 21.379 % |
c |      2077 |   73859   257225 |   44009    2002     6572     3.3 | 21.679 % |
c |      3216 |   73611   256387 |   48410    3119    10494     3.4 | 21.922 % |
c |      4924 |   73374   255578 |   53251    4795    17420     3.6 | 22.159 % |
c |      7486 |   73273   255229 |   58576    7347    30948     4.2 | 22.263 % |
c |     11330 |   73193   254957 |   64433   11181    66052     5.9 | 22.349 % |
c |     17097 |   72998   254278 |   70877   16923   113766     6.7 | 22.546 % |
c |     25746 |   72898   253948 |   77964   25559   224930     8.8 | 22.655 % |
c |     38720 |   72812   253650 |   85761   38517   661634    17.2 | 22.748 % |
c |     58181 |   72606   252964 |   94337   57947  1049806    18.1 | 22.961 % |
c |     87373 |   72196   251542 |  103771   87080  1754152    20.1 | 23.389 % |
c |    131163 |   71972   250802 |  114148   41228  1533805    37.2 | 23.620 % |
c |    196847 |   71591   249499 |  125563  106857  3867118    36.2 | 24.007 % |
c ==============================================================================
c [1mFound solution: 5213604[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 10697   maxlim: 3531185   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206267 |  146356   516564 |   48785  116271  4063017    34.9 | 24.007 % |
c |    206367 |  146356   516564 |   53663   25828   329914    12.8 | 14.909 % |
c |    206517 |  146356   516564 |   59029   25978   330670    12.7 | 14.909 % |
c |    206742 |  146356   516564 |   64932   26203   331902    12.7 | 14.909 % |
c |    207079 |  146356   516564 |   71426   26540   333926    12.6 | 14.909 % |
c |    207585 |  146356   516564 |   78568   27046   337848    12.5 | 14.909 % |
c |    208345 |  146356   516564 |   86425   27806   343207    12.3 | 14.909 % |
c |    209485 |  146356   516564 |   95068   28946   354712    12.3 | 14.909 % |
c |    211194 |  146356   516564 |  104574   30655   438539    14.3 | 14.909 % |
c |    213756 |  146347   516535 |  115032   33216   574341    17.3 | 14.916 % |
c |    217600 |  146347   516535 |  126535   37060   627642    16.9 | 14.916 % |
c |    223366 |  146338   516506 |  139189   42825   694505    16.2 | 14.923 % |
c |    232015 |  146338   516506 |  153108   51474   805129    15.6 | 14.923 % |
c |    244989 |  146304   516396 |  168419   64442   949129    14.7 | 14.948 % |
c |    264450 |  146105   515737 |  185260   83870  1382339    16.5 | 15.080 % |
c |    293643 |  145961   515261 |  203787  113042  2595863    23.0 | 15.176 % |
c ==============================================================================
c [1mFound solution: 4655224[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 4089565   bits: 23/22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    293753 |  145974   515450 |   48658  113152  2598014    23.0 | 15.176 % |
c |    293853 |  145974   515450 |   53523   28686   299095    10.4 | 15.216 % |
c |    294003 |  145974   515450 |   58876   28836   300620    10.4 | 15.216 % |
c |    294228 |  145974   515450 |   64763   29061   302913    10.4 | 15.216 % |
c |    294566 |  145974   515450 |   71240   29399   305777    10.4 | 15.216 % |
c |    295072 |  145974   515450 |   78364   29905   310767    10.4 | 15.216 % |
c |    295831 |  145974   515450 |   86200   30664   317506    10.4 | 15.216 % |
c |    296971 |  145974   515450 |   94820   31804   331724    10.4 | 15.216 % |
c |    298679 |  145974   515450 |  104302   33512   360191    10.7 | 15.216 % |
c |    301241 |  145974   515450 |  114733   36074   386648    10.7 | 15.216 % |
c |    305085 |  145974   515450 |  126206   39918   438818    11.0 | 15.216 % |
c |    310851 |  145958   515398 |  138826   45681   510637    11.2 | 15.226 % |
c |    319502 |  145958   515398 |  152709   54332  1144025    21.1 | 15.226 % |
c |    332476 |  145894   515180 |  167980   67297  1339636    19.9 | 15.266 % |
c |    351937 |  145668   514440 |  184778   86721  1588714    18.3 | 15.415 % |
c |    381129 |  145613   514261 |  203256  115904  4794945    41.4 | 15.451 % |
c |    424919 |  145479   513815 |  223582  159666  5614743    35.2 | 15.537 % |
c ==============================================================================
c [1mFound solution: 3321194[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2   maxlim: 5423595   bits: 24/23
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    426372 |  145485   513933 |   48495  161116  5635088    35.0 | 15.537 % |
c |    426472 |  145485   513933 |   53344   30764   391145    12.7 | 15.582 % |
c |    426622 |  145485   513933 |   58678   30914   391897    12.7 | 15.582 % |
c |    426847 |  145485   513933 |   64546   31139   393038    12.6 | 15.582 % |
c |    427184 |  145485   513933 |   71001   31476   394740    12.5 | 15.582 % |
c |    427690 |  145485   513933 |   78101   31982   397525    12.4 | 15.582 % |
c |    428449 |  145485   513933 |   85911   32741   401906    12.3 | 15.582 % |
c |    429588 |  145485   513933 |   94503   33880   408780    12.1 | 15.582 % |
c |    431296 |  145485   513933 |  103953   35588   433082    12.2 | 15.582 % |
c |    433859 |  145485   513933 |  114348   38151   458649    12.0 | 15.582 % |
c |    437703 |  145485   513933 |  125783   41995   500543    11.9 | 15.582 % |
c |    443471 |  145485   513933 |  138361   47763   566708    11.9 | 15.582 % |
c |    452120 |  145451   513574 |  152198   56407   671014    11.9 | 15.589 % |
c |    465095 |  145442   513543 |  167417   69380   860573    12.4 | 15.592 % |
c |    484558 |  145416   513453 |  184159   88839  1325748    14.9 | 15.607 % |
c |    513750 |  145408   513433 |  202575  118029  4410739    37.4 | 15.614 % |
c |    557540 |  145371   513310 |  222833  161810  6247878    38.6 | 15.635 % |
c |    623224 |  145363   513290 |  245116  227492  9312463    40.9 | 15.642 % |
c |    721750 |  145335   513198 |  269628   87007  4988357    57.3 | 15.660 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 X0_bit_3 -X0_bit_2 X0_bit_1 X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 X1_bit_5 X1_bit_4 X1_bit_3 -X1_bit_2 X1_bit_1 X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 X2_bit_7 -X2_bit_6 X2_bit_5 -X2_bit_4 -X2_bit_3 X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 X3_bit_7 X3_bit_6 X3_bit_5 X3_bit_4 X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 X5_bit_6 -X5_bit_5 X5_bit_4 X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 X8_bit_7 -X8_bit_6 -X8_bit_5 X8_bit_4 X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 X10_bit_6 X10_bit_5 X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 X11_bit_7 X11_bit_6 X11_bit_5 X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 X11_bit0 X11_bit1 X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X12_bit_7 -X12_bit_6 X12_bit_5 -X12_bit_4 X12_bit_3 X12_bit_2 X12_bit_1 X12_bit0 -X12_bit1 -X12_bit2 X12_bit3 -X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 X13_bit_7 -X13_bit_6 X13_bit_5 X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bit8 -X13_bit9 -X13_bit10 -X13_bit11 -X13_bit12 -X14_bit_7 -X14_bit_6 -X14_bit_5 -X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X15_bit_7 X15_bit_6 X15_bit_5 X15_bit_4 X15_bit_3 X15_bit_2 -X15_bit_1 -X15_bit0 -X15_bit1 -X15_bit2 -X15_bit3 -X15_bit4 -X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 X16_bit_3 -X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 -X16_bit2 -X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X17_bit_7 -X17_bit_6 -X17_bit_5 -X17_bit_4 X17_bit_3 -X17_bit_2 X17_bit_1 -X17_bit0 -X17_bit1 X17_bit2 -X17_bit3 -X17_bit4 -X17_bit5 -X17_bit6 -X17_bit7 -X17_bit8 -X17_bit9 -X17_bit10 -X17_bit11 -X17_bit12 -X18_bit_7 -X18_bit_6 -X18_bit_5 -X18_bit_4 -X18_bit_3 -X18_bit_2 -X18_bit_1 -X18_bit0 -X18_bit1 -X18_bit2 -X18_bit3 -X18_bit4 -X18_bit5 -X18_bit6 -X18_bit7 -X18_bit8 -X18_bit9 -X18_bit10 -X18_bit11 -X18_bit12 X19_bit_7 -X19_bit_6 -X19_bit_5 X19_bit_4 X19_bit_3 X19_bit_2 -X19_bit_1 X19_bit0 -X19_bit1 X19_bit2 -X19_bit3 -X19_bit4 -X19_bit5 -X19_bit6 -X19_bit7 -X19_bit8 -X19_bit9 -X19_bit10 -X19_bit11 -X19_bit12 X20_bit_7 -X20_bit_6 -X20_bit_5 -X20_bit_4 -X20_bit_3 -X20_bit_2 -X20_bit_1 -X20_bit0 -X20_bit1 -X20_bit2 -X20_bit3 -X20_bit4 -X20_bit5 -X20_bit6 -X20_bit7 -X20_bit8 -X20_bit9 -X20_bit10 -X20_bit11 -X20_bit12 -X21_bit_7 X21_bit_6 -X21_bit_5 X21_bit_4 X21_bit_3 -X21_bit_2 -X21_bit_1 -X21_bit0 -X21_bit1 -X21_bit2 X21_bit3 -X21_bit4 -X21_bit5 -X21_bit6 -X21_bit7 -X21_bit8 -X21_bit9 -X21_bit10 -X21_bit11 -X21_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 -X22_bit2 -X22_bit3 -X22_bit4 -X22_bit5 -X22_bit6 -X22_bit7 -X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 -X23_bit0 -X23_bit1 -X23_bit2 -X23_bit3 -X23_bit4 -X23_bit5 -X23_bit6 -X23_bit7 -X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 X24_bit_7 -X24_bit_6 -X24_bit_5 X24_bit_4 X24_bit_3 X24_bit_2 X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 X25_bit_2 X25_bit_1 -X25_bit0 X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 -X26_bit0 -X26_bit1 -X26_bit2 -X26_bit3 -X26_bit4 -X26_bit5 -X26_bit6 -X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X27_bit_7 -X27_bit_6 -X27_bit_5 -X27_bit_4 -X27_bit_3 -X27_bit_2 -X27_bit_1 -X27_bit0 -X27_bit1 -X27_bit2 -X27_bit3 -X27_bit4 -X27_bit5 -X27_bit6 -X27_bit7 -X27_bit8 -X27_bit9 -X27_bit10 -X27_bit11 -X27_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 X31_bit_5 X31_bit_4 -X31_bit_3 X31_bit_2 X31_bit_1 X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X32_bit_7 -X32_bit_6 -X32_bit_5 -X32_bit_4 -X32_bit_3 -X32_bit_2 -X32_bit_1 -X32_bit0 -X32_bit1 -X32_bit2 -X32_bit3 -X32_bit4 -X32_bit5 -X32_bit6 -X32_bit7 -X32_bit8 -X32_bit9 -X32_bit10 -X32_bit11 -X32_bit12 X33_bit_7 -X33_bit_6 -X33_bit_5 -X33_bit_4 -X33_bit_3 -X33_bit_2 -X33_bit_1 -X33_bit0 -X33_bit1 -X33_bit2 -X33_bit3 -X33_bit4 -X33_bit5 -X33_bit6 -X33_bit7 -X33_bit8 -X33_bit9 -X33_bit10 -X33_bit11 -X33_bit12 -X34_bit_7 -X34_bit_6 X34_bit_5 -X34_bit_4 -X34_bit_3 -X34_bit_2 -X34_bit_1 -X34_bit0 -X34_bit1 -X34_bit2 -X34_bit3 -X34_bit4 -X34_bit5 -X34_bit6 -X34_bit7 -X34_bit8 -X34_bit9 -X34_bit10 -X34_bit11 -X34_bit12 -X35_bit_7 -X35_bit_6 -X35_bit_5 -X35_bit_4 -X35_bit_3 -X35_bit_2 -X35_bit_1 -X35_bit0 -X35_bit1 -X35_bit2 -X35_bit3 -X35_bit4 -X35_bit5 -X35_bit6 -X35_bit7 -X35_bit8 -X35_bit9 -X35_bit10 -X35_bit11 -X35_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 -X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 -X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 -X37_bit_2 -X37_bit_1 X37_bit0 -X37_bit1 -X37_bit2 -X37_bit3 -X37_bit4 -X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 X38_bit_3 X38_bit_2 X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X40_bit_7 -X40_bit_6 -X40_bit_5 -X40_bit_4 -X40_bit_3 X40_bit_2 X40_bit_1 -X40_bit0 -X40_bit1 -X40_bit2 -X40_bit3 -X40_bit4 -X40_bit5 -X40_bit6 -X40_bit7 -X40_bit8 -X40_bit9 -X40_bit10 -X40_bit11 -X40_bit12 X41_bit_7 X41_bit_6 -X41_bit_5 -X41_bit_4 -X41_bit_3 X41_bit_2 -X41_bit_1 -X41_bit0 X41_bit1 -X41_bit2 -X41_bit3 -X41_bit4 -X41_bit5 -X41_bit6 -X41_bit7 -X41_bit8 -X41_bit9 -X41_bit10 -X41_bit11 -X41_bit12 -X42_bit_7 X42_bit_6 X42_bit_5 X42_bit_4 -X42_bit_3 -X42_bit_2 -X42_bit_1 -X42_bit0 -X42_bit1 -X42_bit2 -X42_bit3 -X42_bit4 -X42_bit5 -X42_bit6 -X42_bit7 -X42_bit8 -X42_bit9 -X42_bit10 -X42_bit11 -X42_bit12 X43_bit_7 X43_bit_6 -X43_bit_5 X43_bit_4 X43_bit_3 X43_bit_2 -X43_bit_1 -X43_bit0 X43_bit1 -X43_bit2 -X43_bit3 -X43_bit4 -X43_bit5 -X43_bit6 -X43_bit7 -X43_bit8 -X43_bit9 -X43_bit10 -X43_bit11 -X43_bit12 X44_bit_7 -X44_bit_6 X44_bit_5 -X44_bit_4 X44_bit_3 X44_bit_2 X44_bit_1 X44_bit0 -X44_bit1 -X44_bit2 -X44_bit3 -X44_bit4 -X44_bit5 -X44_bit6 -X44_bit7 -X44_bit8 -X44_bit9 -X44_bit10 -X44_bit11 -X44_bit12 X45_bit_7 -X45_bit_6 X45_bit_5 X45_bit_4 -X45_bit_3 -X45_bit_2 -X45_bit_1 -X45_bit0 -X45_bit1 -X45_bit2 -X45_bit3 -X45_bit4 -X45_bit5 -X45_bit6 -X45_bit7 -X45_bit8 -X45_bit9 -X45_bit10 -X45_bit11 -X45_bit12 X46_bit_7 X46_bit_6 -X46_bit_5 X46_bit_4 X46_bit_3 X46_bit_2 -X46_bit_1 -X46_bit0 -X46_bit1 -X46_bit2 -X46_bit3 -X46_bit4 -X46_bit5 -X46_bit6 -X46_bit7 -X46_bit8 -X46_bit9 -X46_bit10 -X46_bit11 -X46_bit12 -X47_bit_7 -X47_bit_6 -X47_bit_5 -X47_bit_4 -X47_bit_3 -X47_bit_2 -X47_bit_1 -X47_bit0 -X47_bit1 -X47_bit2 -X47_bit3 -X47_bit4 -X47_bit5 -X47_bit6 -X47_bit7 -X47_bit8 -X47_bit9 -X47_bit10 -X47_bit11 -X47_bit12 X48_bit_7 X48_bit_6 -X48_bit_5 X48_bit_4 X48_bit_3 X48_bit_2 -X48_bit_1 -X48_bit0 -X48_bit1 -X48_bit2 -X48_bit3 -X48_bit4 -X48_bit5 -X48_bit6 -X48_bit7 -X48_bit8 -X48_bit9 -X48_bit10 -X48_bit11 -X48_bit12 -X49_bit_7 X49_bit_6 -X49_bit_5 X49_bit_4 X49_bit_3 -X49_bit_2 -X49_bit_1 -X49_bit0 -X49_bit1 -X49_bit2 -X49_bit3 -X49_bit4 -X49_bit5 -X49_bit6 -X49_bit7 -X49_bit8 -X49_bit9 -X49_bit10 -X49_bit11 -X49_bit12 X50_bit_7 -X50_bit_6 -X50_bit_5 X50_bit_4 -X50_bit_3 X50_bit_2 -X50_bit_1 -X50_bit0 -X50_bit1 -X50_bit2 -X50_bit3 -X50_bit4 -X50_bit5 -X50_bit6 -X50_bit7 -X50_bit8 -X50_bit9 -X50_bit10 -X50_bit11 -X50_bit12 -X51_bit_7 -X51_bit_6 -X51_bit_5 -X51_bit_4 -X51_bit_3 -X51_bit_2 -X51_bit_1 -X51_bit0 -X51_bit1 -X51_bit2 -X51_bit3 -X51_bit4 -X51_bit5 -X51_bit6 -X51_bit7 -X51_bit8 -X51_bit9 -X51_bit10 -X51_bit11 -X51_bit12 -X52_bit_7 X52_bit_6 -X52_bit_5 -X52_bit_4 -X52_bit_3 -X52_bit_2 -X52_bit_1 -X52_bit0 -X52_bit1 -X52_bit2 -X52_bit3 -X52_bit4 -X52_bit5 -X52_bit6 -X52_bit7 -X52_bit8 -X52_bit9 -X52_bit10 -X52_bit11 -X52_bit12 X53_bit_7 X53_bit_6 -X53_bit_5 -X53_bit_4 -X53_bit_3 -X53_bit_2 -X53_bit_1 -X53_bit0 -X53_bit1 -X53_bit2 -X53_bit3 -X53_bit4 -X53_bit5 -X53_bit6 -X53_bit7 -X53_bit8 -X53_bit9 -X53_bit10 -X53_bit11 -X53_bit12 -X54_bit_7 -X54_bit_6 -X54_bit_5 -X54_bit_4 -X54_bit_3 -X54_bit_2 -X54_bit_1 -X54_bit0 -X54_bit1 -X54_bit2 -X54_bit3 -X54_bit4 -X54_bit5 -X54_bit6 -X54_bit7 -X54_bit8 -X54_bit9 -X54_bit10 -X54_bit11 -X54_bit12 -X55_bit_7 X55_bit_6 -X55_bit_5 X55_bit_4 X55_bit_3 X55_bit_2 -X55_bit_1 -X55_bit0 -X55_bit1 -X55_bit2 -X55_bit3 -X55_bit4 -X55_bit5 -X55_bit6 -X55_bit7 -X55_bit8 -X55_bit9 -X55_bit10 -X55_bit11 -X55_bit12 X56_bit_7 -X56_bit_6 -X56_bit_5 -X56_bit_4 X56_bit_3 X56_bit_2 X56_bit_1 -X56_bit0 -X56_bit1 -X56_bit2 -X56_bit3 -X56_bit4 -X56_bit5 -X56_bit6 -X56_bit7 -X56_bit8 -X56_bit9 -X56_bit10 -X56_bit11 -X56_bit12 -X57_bit_7 -X57_bit_6 -X57_bit_5 -X57_bit_4 -X57_bit_3 -X57_bit_2 -X57_bit_1 -X57_bit0 -X57_bit1 -X57_bit2 -X57_bit3 -X57_bit4 -X57_bit5 -X57_bit6 -X57_bit7 -X57_bit8 -X57_bit9 -X57_bit10 -X57_bit11 -X57_bit12 -X58_bit_7 -X58_bit_6 -X58_bit_5 -X58_bit_4 -X58_bit_3 -X58_bit_2 -X58_bit_1 -X58_bit0 -X58_bit1 -X58_bit2 -X58_bit3 -X58_bit4 -X58_bit5 -X58_bit6 -X58_bit7 -X58_bit8 -X58_bit9 -X58_bit10 -X58_bit11 -X58_bit12 -X59_bit_7 -X59_bit_6 -X59_bit_5 -X59_bit_4 -X59_bit_3 -X59_bit_2 -X59_bit_1 -X59_bit0 -X59_bit1 -X59_bit2 -X59_bit3 -X59_bit4 -X59_bit5 -X59_bit6 -X59_bit7 -X59_bit8 -X59_bit9 -X59_bit10 -X59_bit11 -X59_bit12 -X60_bit_7 -X60_bit_6 -X60_bit_5 -X60_bit_4 X60_bit_3 -X60_bit_2 -X60_bit_1 -X60_bit0 -X60_bit1 -X60_bit2 -X60_bit3 -X60_bit4 -X60_bit5 -X60_bit6 -X60_bit7 -X60_bit8 -X60_bit9 -X60_bit10 -X60_bit11 -X60_bit12 -X61_bit_7 -X61_bit_6 -X61_bit_5 X61_bit_4 -X61_bit_3 -X61_bit_2 -X61_bit_1 -X61_bit0 -X61_bit1 -X61_bit2 -X61_bit3 -X61_bit4 -X61_bit5 -X61_bit6 -X61_bit7 -X61_bit8 -X61_bit9 -X61_bit10 -X61_bit11 -X61_bit12 -X62_bit_7 X62_bit_6 -X62_bit_5 X62_bit_4 X62_bit_3 X62_bit_2 -X62_bit_1 -X62_bit0 -X62_bit1 -X62_bit2 -X62_bit3 -X62_bit4 -X62_bit5 -X62_bit6 -X62_bit7 -X62_bit8 -X62_bit9 -X62_bit10 -X62_bit11 -X62_bit12 -X63_bit_7 -X63_bit_6 -X63_bit_5 -X63_bit_4 -X63_bit_3 -X63_bit_2 -X63_bit_1 -X63_bit0 -X63_bit1 -X63_bit2 -X63_bit3 -X63_bit4 -X63_bit5 -X63_bit6 -X63_bit7 -X63_bit8 -X63_bit9 -X63_bit10 -X63_bit11 -X63_bit12 X64_bit_7 X64_bit_6 -X64_bit_5 X64_bit_4 X64_bit_3 X64_bit_2 -X64_bit_1 -X64_bit0 -X64_bit1 -X64_bit2 -X64_bit3 -X64_bit4 -X64_bit5 -X64_bit6 -X64_bit7 -X64_bit8 -X64_bit9 -X64_bit10 -X64_bit11 -X64_bit12 -X65_bit_7 -X65_bit_6 -X65_bit_5 -X65_bit_4 -X65_bit_3 -X65_bit_2 -X65_bit_1 -X65_bit0 -X65_bit1 -X65_bit2 -X65_bit3 -X65_bit4 -X65_bit5 -X65_bit6 -X65_bit7 -X65_bit8 -X65_bit9 -X65_bit10 -X65_bit11 -X65_bit12 X66_bit_7 -X66_bit_6 -X66_bit_5 X66_bit_4 -X66_bit_3 -X66_bit_2 -X66_bit_1 -X66_bit0 -X66_bit1 -X66_bit2 -X66_bit3 -X66_bit4 -X66_bit5 -X66_bit6 -X66_bit7 -X66_bit8 -X66_bit9 -X66_bit10 -X66_bit11 -X66_bit12 X67_bit_7 -X67_bit_6 X67_bit_5 -X67_bit_4 -X67_bit_3 X67_bit_2 X67_bit_1 X67_bit0 X67_bit1 -X67_bit2 -X67_bit3 -X67_bit4 -X67_bit5 -X67_bit6 -X67_bit7 -X67_bit8 -X67_bit9 -X67_bit10 -X67_bit11 -X67_bit12 X68_bit_7 X68_bit_6 -X68_bit_5 -X68_bit_4 -X68_bit_3 X68_bit_2 -X68_bit_1 -X68_bit0 -X68_bit1 -X68_bit2 -X68_bit3 -X68_bit4 -X68_bit5 -X68_bit6 -X68_bit7 -X68_bit8 -X68_bit9 -X68_bit10 -X68_bit11 -X68_bit12 X69_bit_7 X69_bit_6 -X69_bit_5 X69_bit_4 X69_bit_3 X69_bit_2 -X69_bit_1 -X69_bit0 X69_bit1 -X69_bit2 -X69_bit3 -X69_bit4 -X69_bit5 -X69_bit6 -X69_bit7 -X69_bit8 -X69_bit9 -X69_bit10 -X69_bit11 -X69_bit12 X70_bit_7 X70_bit_6 -X70_bit_5 X70_bit_4 X70_bit_3 X70_bit_2 -X70_bit_1 -X70_bit0 -X70_bit1 -X70_bit2 -X70_bit3 -X70_bit4 -X70_bit5 -X70_bit6 -X70_bit7 -X70_bit8 -X70_bit9 -X70_bit10 -X70_bit11 -X70_bit12 -X71_bit_7 X71_bit_6 -X71_bit_5 X71_bit_4 X71_bit_3 X71_bit_2 -X71_bit_1 X71_bit0 -X71_bit1 -X71_bit2 -X71_bit3 -X71_bit4 -X71_bit5 -X71_bit6 -X71_bit7 -X71_bit8 -X71_bit9 -X71_bit10 -X71_bit11 -X71_bit12 X72_bit_7 -X72_bit_6 -X72_bit_5 -X72_bit_4 X72_bit_3 X72_bit_2 X72_bit_1 -X72_bit0 -X72_bit1 -X72_bit2 -X72_bit3 -X72_bit4 -X72_bit5 -X72_bit6 -X72_bit7 -X72_bit8 -X72_bit9 -X72_bit10 -X72_bit11 -X72_bit12 -X73_bit_7 -X73_bit_6 -X73_bit_5 -X73_bit_4 -X73_bit_3 -X73_bit_2 -X73_bit_1 -X73_bit0 -X73_bit1 -X73_bit2 -X73_bit3 -X73_bit4 -X73_bit5 -X73_bit6 -X73_bit7 -X73_bit8 -X73_bit9 -X73_bit10 -X73_bit11 -X73_bit12 -X74_bit_7 -X74_bit_6 X74_bit_5 -X74_bit_4 -X74_bit_3 X74_bit_2 -X74_bit_1 -X74_bit0 -X74_bit1 -X74_bit2 -X74_bit3 -X74_bit4 -X74_bit5 -X74_bit6 -X74_bit7 -X74_bit8 -X74_bit9 -X74_bit10 -X74_bit11 -X74_bit12 X75_bit_7 -X75_bit_6 X75_bit_5 X75_bit_4 -X75_bit_3 X75_bit_2 X75_bit_1 -X75_bit0 -X75_bit1 -X75_bit2 -X75_bit3 -X75_bit4 -X75_bit5 -X75_bit6 -X75_bit7 -X75_bit8 -X75_bit9 -X75_bit10 -X75_bit11 -X75_bit12 X76_bit_7 X76_bit_6 -X76_bit_5 -X76_bit_4 -X76_bit_3 X76_bit_2 X76_bit_1 X76_bit0 -X76_bit1 -X76_bit2 -X76_bit3 -X76_bit4 -X76_bit5 -X76_bit6 -X76_bit7 -X76_bit8 -X76_bit9 -X76_bit10 -X76_bit11 -X76_bit12 -X77_bit_7 -X77_bit_6 X77_bit_5 X77_bit_4 -X77_bit_3 -X77_bit_2 -X77_bit_1 -X77_bit0 -X77_bit1 -X77_bit2 -X77_bit3 -X77_bit4 -X77_bit5 -X77_bit6 -X77_bit7 -X77_bit8 -X77_bit9 -X77_bit10 -X77_bit11 -X77_bit12 X78_bit_7 X78_bit_6 X78_bit_5 X78_bit_4 X78_bit_3 X78_bit_2 -X78_bit_1 -X78_bit0 X78_bit1 -X78_bit2 -X78_bit3 -X78_bit4 -X78_bit5 -X78_bit6 -X78_bit7 -X78_bit8 -X78_bit9 -X78_bit10 -X78_bit11 -X78_bit12 -X79_bit_7 -X79_bit_6 X79_bit_5 -X79_bit_4 X79_bit_3 -X79_bit_2 X79_bit_1 -X79_bit0 X79_bit1 -X79_bit2 -X79_bit3 -X79_bit4 -X79_bit5 -X79_bit6 -X79_bit7 -X79_bit8 -X79_bit9 -X79_bit10 -X79_bit11 -X79_bit12 -X80_bit_7 -X80_bit_6 -X80_bit_5 -X80_bit_4 -X80_bit_3 -X80_bit_2 -X80_bit_1 -X80_bit0 -X80_bit1 -X80_bit2 -X80_bit3 -X80_bit4 -X80_bit5 -X80_bit6 -X80_bit7 -X80_bit8 -X80_bit9 -X80_bit10 -X80_bit11 -X80_bit12 -X81_bit_7 -X81_bit_6 X81_bit_5 -X81_bit_4 X81_bit_3 -X81_bit_2 -X81_bit_1 X81_bit0 -X81_bit1 -X81_bit2 -X81_bit3 -X81_bit4 -X81_bit5 -X81_bit6 -X81_bit7 -X81_bit8 -X81_bit9 -X81_bit10 -X81_bit11 -X81_bit12 -X82_bit_7 -X82_bit_6 -X82_bit_5 -X82_bit_4 -X82_bit_3 -X82_bit_2 -X82_bit_1 -X82_bit0 -X82_bit1 -X82_bit2 -X82_bit3 -X82_bit4 -X82_bit5 -X82_bit6 -X82_bit7 -X82_bit8 -X82_bit9 -X82_bit10 -X82_bit11 -X82_bit12 -X83_bit_7 -X83_bit_6 -X83_bit_5 -X83_bit_4 -X83_bit_3 -X83_bit_2 -X83_bit_1 -X83_bit0 -X83_bit1 -X83_bit2 -X83_bit3 -X83_bit4 -X83_bit5 -X83_bit6 -X83_bit7 -X83_bit8 -X83_bit9 -X83_bit10 -X83_bit11 -X83_bit12 -X84_bit_7 X84_bit_6 -X84_bit_5 -X84_bit_4 X84_bit_3 X84_bit_2 X84_bit_1 -X84_bit0 -X84_bit1 -X84_bit2 -X84_bit3 -X84_bit4 -X84_bit5 -X84_bit6 -X84_bit7 -X84_bit8 -X84_bit9 -X84_bit10 -X84_bit11 -X84_bit12 X85_bit_7 -X85_bit_6 -X85_bit_5 -X85_bit_4 X85_bit_3 X85_bit_2 X85_bit_1 -X85_bit0 X85_bit1 -X85_bit2 -X85_bit3 -X85_bit4 -X85_bit5 -X85_bit6 -X85_bit7 -X85_bit8 -X85_bit9 -X85_bit10 -X85_bit11 -X85_bit12 -X86_bit_7 -X86_bit_6 -X86_bit_5 -X86_bit_4 -X86_bit_3 -X86_bit_2 -X86_bit_1 -X86_bit0 -X86_bit1 -X86_bit2 -X86_bit3 -X86_bit4 -X86_bit5 -X86_bit6 -X86_bit7 -X86_bit8 -X86_bit9 -X86_bit10 -X86_bit11 -X86_bit12 -X87_bit_7 -X87_bit_6 -X87_bit_5 -X87_bit_4 -X87_bit_3 -X87_bit_2 -X87_bit_1 -X87_bit0 -X87_bit1 -X87_bit2 -X87_bit3 -X87_bit4 -X87_bit5 -X87_bit6 -X87_bit7 -X87_bit8 -X87_bit9 -X87_bit10 -X87_bit11 -X87_bit12 -X88_bit_7 -X88_bit_6 -X88_bit_5 -X88_bit_4 -X88_bit_3 -X88_bit_2 -X88_bit_1 -X88_bit0 -X88_bit1 -X88_bit2 -X88_bit3 -X88_bit4 -X88_bit5 -X88_bit6 -X88_bit7 -X88_bit8 -X88_bit9 -X88_bit10 -X88_bit11 -X88_bit12 X89_bit_7 -X89_bit_6 -X89_bit_5 X89_bit_4 X89_bit_3 X89_bit_2 X89_bit_1 X89_bit0 -X89_bit1 -X89_bit2 -X89_bit3 -X89_bit4 -X89_bit5 -X89_bit6 -X89_bit7 -X89_bit8 -X89_bit9 -X89_bit10 -X89_bit11 -X89_bit12 -X90_bit_7 -X90_bit_6 -X90_bit_5 -X90_bit_4 X90_bit_3 -X90_bit_2 -X90_bit_1 -X90_bit0 -X90_bit1 -X90_bit2 -X90_bit3 -X90_bit4 -X90_bit5 -X90_bit6 -X90_bit7 -X90_bit8 -X90_bit9 -X90_bit10 -X90_bit11 -X90_bit12 X91_bit_7 -X91_bit_6 -X91_bit_5 X91_bit_4 X91_bit_3 X91_bit_2 X91_bit_1 X91_bit0 X91_bit1 X91_bit2 -X91_bit3 X91_bit4 -X91_bit5 -X91_bit6 -X91_bit7 -X91_bit8 -X91_bit9 -X91_bit10 -X91_bit11 -X91_bit12 X92_bit_7 -X92_bit_6 -X92_bit_5 X92_bit_4 X92_bit_3 X92_bit_2 -X92_bit_1 -X92_bit0 -X92_bit1 -X92_bit2 -X92_bit3 -X92_bit4 -X92_bit5 -X92_bit6 -X92_bit7 -X92_bit8 -X92_bit9 -X92_bit10 -X92_bit11 -X92_bit12 X93_bit_7 -X93_bit_6 X93_bit_5 -X93_bit_4 X93_bit_3 -X93_bit_2 -X93_bit_1 -X93_bit0 -X93_bit1 -X93_bit2 -X93_bit3 -X93_bit4 -X93_bit5 -X93_bit6 -X93_bit7 -X93_bit8 -X93_bit9 -X93_bit10 -X93_bit11 -X93_bit12 X94_bit_7 -X94_bit_6 -X94_bit_5 X94_bit_4 X94_bit_3 X94_bit_2 -X94_bit_1 -X94_bit0 X94_bit1 X94_bit2 -X94_bit3 X94_bit4 -X94_bit5 -X94_bit6 -X94_bit7 -X94_bit8 -X94_bit9 -X94_bit10 -X94_bit11 -X94_bit12 -X95_bit_7 -X95_bit_6 -X95_bit_5 -X95_bit_4 -X95_bit_3 -X95_bit_2 -X95_bit_1 -X95_bit0 -X95_bit1 -X95_bit2 -X95_bit3 -X95_bit4 -X95_bit5 -X95_bit6 -X95_bit7 -X95_bit8 -X95_bit9 -X95_bit10 -X95_bit11 -X95_bit12 X96_bit_7 X96_bit_6 X96_bit_5 -X96_bit_4 -X96_bit_3 X96_bit_2 -X96_bit_1 X96_bit0 -X96_bit1 -X96_bit2 -X96_bit3 -X96_bit4 -X96_bit5 -X96_bit6 -X96_bit7 -X96_bit8 -X96_bit9 -X96_bit10 -X96_bit11 -X96_bit12 -X97_bit_7 -X97_bit_6 -X97_bit_5 -X97_bit_4 -X97_bit_3 -X97_bit_2 -X97_bit_1 -X97_bit0 -X97_bit1 -X97_bit2 -X97_bit3 -X97_bit4 -X97_bit5 -X97_bit6 -X97_bit7 -X97_bit8 -X97_bit9 -X97_bit10 -X97_bit11 -X97_bit12 X98_bit_7 -X98_bit_6 X98_bit_5 -X98_bit_4 -X98_bit_3 -X98_bit_2 -X98_bit_1 -X98_bit0 -X98_bit1 -X98_bit2 -X98_bit3 -X98_bit4 -X98_bit5 -X98_bit6 -X98_bit7 -X98_bit8 -X98_bit9 -X98_bit10 -X98_bit11 -X98_bit12 X99_bit_7 -X99_bit_6 -X99_bit_5 X99_bit_4 X99_bit_3 X99_bit_2 -X99_bit_1 X99_bit0 -X99_bit1 -X99_bit2 -X99_bit3 -X99_bit4 -X99_bit5 -X99_bit6 -X99_bit7 -X99_bit8 -X99_bit9 -X99_bit10 -X99_bit11 -X99_bit12 X100_bit_7 X100_bit_6 -X100_bit_5 -X100_bit_4 -X100_bit_3 -X100_bit_2 -X100_bit_1 -X100_bit0 -X100_bit1 -X100_bit2 -X100_bit3 -X100_bit4 -X100_bit5 -X100_bit6 -X100_bit7 -X100_bit8 -X100_bit9 -X100_bit10 -X100_bit11 -X100_bit12 -X101_bit_7 X101_bit_6 -X101_bit_5 X101_bit_4 -X101_bit_3 -X101_bit_2 X101_bit_1 -X101_bit0 -X101_bit1 -X101_bit2 -X101_bit3 -X101_bit4 -X101_bit5 -X101_bit6 -X101_bit7 -X101_bit8 -X101_bit9 -X101_bit10 -X101_bit11 -X101_bit12 -X102_bit_7 -X102_bit_6 -X102_bit_5 -X102_bit_4 -X102_bit_3 -X102_bit_2 -X102_bit_1 -X102_bit0 -X102_bit1 -X102_bit2 -X102_bit3 -X102_bit4 -X102_bit5 -X102_bit6 -X102_bit7 -X102_bit8 -X102_bit9 -X102_bit10 -X102_bit11 -X102_bit12 -X103_bit_7 -X103_bit_6 -X103_bit_5 -X103_bit_4 -X103_bit_3 -X103_bit_2 -X103_bit_1 -X103_bit0 -X103_bit1 -X103_bit2 -X103_bit3 -X103_bit4 -X103_bit5 -X103_bit6 -X103_bit7 -X103_bit8 -X103_bit9 -X103_bit10 -X103_bit11 -X103_bit12 X104_bit_7 X104_bit_6 X104_bit_5 -X104_bit_4 -X104_bit_3 X104_bit_2 -X104_bit_1 -X104_bit0 -X104_bit1 -X104_bit2 -X104_bit3 -X104_bit4 -X104_bit5 -X104_bit6 -X104_bit7 -X104_bit8 -X104_bit9 -X104_bit10 -X104_bit11 -X104_bit12 X105_bit_7 X105_bit_6 X105_bit_5 -X105_bit_4 X105_bit_3 -X105_bit_2 -X105_bit_1 X105_bit0 X105_bit1 -X105_bit2 -X105_bit3 -X105_bit4 -X105_bit5 -X105_bit6 -X105_bit7 -X105_bit8 -X105_bit9 -X105_bit10 -X105_bit11 -X105_bit12 -X106_bit_7 -X106_bit_6 X106_bit_5 -X106_bit_4 -X106_bit_3 -X106_bit_2 -X106_bit_1 -X106_bit0 -X106_bit1 -X106_bit2 -X106_bit3 -X106_bit4 -X106_bit5 -X106_bit6 -X106_bit7 -X106_bit8 -X106_bit9 -X106_bit10 -X106_bit11 -X106_bit12 -X107_bit_7 -X107_bit_6 X107_bit_5 X107_bit_4 -X107_bit_3 X107_bit_2 -X107_bit_1 X107_bit0 -X107_bit1 -X107_bit2 -X107_bit3 -X107_bit4 -X107_bit5 -X107_bit6 -X107_bit7 -X107_bit8 -X107_bit9 -X107_bit10 -X107_bit11 -X107_bit12 -X108_bit_7 -X108_bit_6 -X108_bit_5 -X108_bit_4 -X108_bit_3 -X108_bit_2 -X108_bit_1 -X108_bit0 -X108_bit1 -X108_bit2 -X108_bit3 -X108_bit4 -X108_bit5 -X108_bit6 -X108_bit7 -X108_bit8 -X108_bit9 -X108_bit10 -X108_bit11 -X108_bit12 -X109_bit_7 -X109_bit_6 -X109_bit_5 -X109_bit_4 -X109_bit_3 -X109_bit_2 -X109_bit_1 -X109_bit0 -X109_bit1 -X109_bit2 -X109_bit3 -X109_bit4 -X109_bit5 -X109_bit6 -X109_bit7 -X109_bit8 -X109_bit9 -X109_bit10 -X109_bit11 -X109_bit12 -X110_bit_7 -X110_bit_6 -X110_bit_5 -X110_bit_4 -X110_bit_3 -X110_bit_2 -X110_bit_1 -X110_bit0 -X110_bit1 -X110_bit2 -X110_bit3 -X110_bit4 -X110_bit5 -X110_bit6 -X110_bit7 -X110_bit8 -X110_bit9 -X110_bit10 -X110_bit11 -X110_bit12 -X111_bit_7 -X111_bit_6 -X111_bit_5 -X111_bit_4 -X111_bit_3 X111_bit_2 X111_bit_1 -X111_bit0 -X111_bit1 -X111_bit2 -X111_bit3 -X111_bit4 -X111_bit5 -X111_bit6 -X111_bit7 -X111_bit8 -X111_bit9 -X111_bit10 -X111_bit11 -X111_bit12 -X112_bit_7 -X112_bit_6 X112_bit_5 -X112_bit_4 -X112_bit_3 X112_bit_2 -X112_bit_1 -X112_bit0 -X112_bit1 -X112_bit2 -X112_bit3 -X112_bit4 -X112_bit5 -X112_bit6 -X112_bit7 -X112_bit8 -X112_bit9 -X112_bit10 -X112_bit11 -X112_bit12 -X113_bit_7 -X113_bit_6 -X113_bit_5 -X113_bit_4 -X113_bit_3 -X113_bit_2 -X113_bit_1 -X113_bit0 -X113_bit1 -X113_bit2 -X113_bit3 -X113_bit4 -X113_bit5 -X113_bit6 -X113_bit7 -X113_bit8 -X113_bit9 -X113_bit10 -X113_bit11 -X113_bit12 -X114_bit_7 -X114_bit_6 X114_bit_5 -X114_bit_4 -X114_bit_3 -X114_bit_2 -X114_bit_1 -X114_bit0 -X114_bit1 -X114_bit2 -X114_bit3 -X114_bit4 -X114_bit5 -X114_bit6 -X114_bit7 -X114_bit8 -X114_bit9 -X114_bit10 -X114_bit11 -X114_bit12 -X115_bit_7 -X115_bit_6 -X115_bit_5 -X115_bit_4 -X115_bit_3 -X115_bit_2 -X115_bit_1 -X115_bit0 -X115_bit1 -X115_bit2 -X115_bit3 X115_bit4 -X115_bit5 -X115_bit6 -X115_bit7 -X115_bit8 -X115_bit9 -X115_bit10 -X115_bit11 -X115_bit12 X116_bit_7 X116_bit_6 -X116_bit_5 -X116_bit_4 -X116_bit_3 -X116_bit_2 -X116_bit_1 -X116_bit0 -X116_bit1 -X116_bit2 -X116_bit3 -X116_bit4 -X116_bit5 -X116_bit6 -X116_bit7 -X116_bit8 -X116_bit9 -X116_bit10 -X116_bit11 -X116_bit12 -X117_bit_7 -X117_bit_6 -X117_bit_5 -X117_bit_4 -X117_bit_3 -X117_bit_2 -X117_bit_1 -X117_bit0 -X117_bit1 -X117_bit2 -X117_bit3 -X117_bit4 -X117_bit5 -X117_bit6 -X117_bit7 -X117_bit8 -X117_bit9 -X117_bit10 -X117_bit11 -X117_bit12 -X118_bit_7 -X118_bit_6 -X118_bit_5 -X118_bit_4 -X118_bit_3 -X118_bit_2 -X118_bit_1 -X118_bit0 -X118_bit1 -X118_bit2 -X118_bit3 -X118_bit4 -X118_bit5 -X118_bit6 -X118_bit7 -X118_bit8 -X118_bit9 -X118_bit10 -X118_bit11 -X118_bit12 X119_bit_7 -X119_bit_6 -X119_bit_5 -X119_bit_4 X119_bit_3 -X119_bit_2 X119_bit_1 -X119_bit0 -X119_bit1 -X119_bit2 -X119_bit3 -X119_bit4 -X119_bit5 -X119_bit6 -X119_bit7 -X119_bit8 -X119_bit9 -X119_bit10 -X119_bit11 -X119_bit12 -X120_bit_7 -X120_bit_6 -X120_bit_5 -X120_bit_4 -X120_bit_3 -X120_bit_2 -X120_bit_1 -X120_bit0 -X120_bit1 -X120_bit2 -X120_bit3 -X120_bit4 -X120_bit5 -X120_bit6 -X120_bit7 -X120_bit8 -X120_bit9 -X120_bit10 -X120_bit11 -X120_bit12 -X121_bit_7 -X121_bit_6 -X121_bit_5 -X121_bit_4 -X121_bit_3 -X121_bit_2 -X121_bit_1 -X121_bit0 -X121_bit1 -X121_bit2 -X121_bit3 -X121_bit4 -X121_bit5 -X121_bit6 -X121_bit7 -X121_bit8 -X121_bit9 -X121_bit10 -X121_bit11 -X121_bit12 -X122_bit_7 -X122_bit_6 -X122_bit_5 -X122_bit_4 -X122_bit_3 -X122_bit_2 -X122_bit_1 -X122_bit0 -X122_bit1 -X122_bit2 -X122_bit3 -X122_bit4 -X122_bit5 -X122_bit6 -X122_bit7 -X122_bit8 -X122_bit9 -X122_bit10 -X122_bit11 -X122_bit12 -X123_bit_7 -X123_bit_6 -X123_bit_5 -X123_bit_4 -X123_bit_3 -X123_bit_2 -X123_bit_1 -X123_bit0 -X123_bit1 -X123_bit2 -X123_bit3 -X123_bit4 -X123_bit5 -X123_bit6 -X123_bit7 -X123_bit8 -X123_bit9 -X123_bit10 -X123_bit11 -X123_bit12 -X124_bit_7 -X124_bit_6 -X124_bit_5 -X124_bit_4 -X124_bit_3 -X124_bit_2 -X124_bit_1 -X124_bit0 -X124_bit1 -X124_bit2 -X124_bit3 -X124_bit4 -X124_bit5 -X124_bit6 -X124_bit7 -X124_bit8 -X124_bit9 -X124_bit10 -X124_bit11 -X124_bit12 -X125_bit_7 -X125_bit_6 X125_bit_5 -X125_bit_4 -X125_bit_3 -X125_bit_2 -X125_bit_1 -X125_bit0 -X125_bit1 -X125_bit2 -X125_bit3 -X125_bit4 -X125_bit5 -X125_bit6 -X125_bit7 -X125_bit8 -X125_bit9 -X125_bit10 -X125_bit11 -X125_bit12 -X126_bit_7 -X126_bit_6 -X126_bit_5 -X126_bit_4 -X126_bit_3 -X126_bit_2 -X126_bit_1 -X126_bit0 -X126_bit1 -X126_bit2 -X126_bit3 -X126_bit4 -X126_bit5 -X126_bit6 -X126_bit7 -X126_bit8 -X126_bit9 -X126_bit10 -X126_bit11 -X126_bit12 -X127_bit_7 -X127_bit_6 -X127_bit_5 -X127_bit_4 -X127_bit_3 -X127_bit_2 -X127_bit_1 -X127_bit0 -X127_bit1 -X127_bit2 -X127_bit3 -X127_bit4 -X127_bit5 -X127_bit6 -X127_bit7 -X127_bit8 -X127_bit9 -X127_bit10 -X127_bit11 -X127_bit12 X128_bit_7 X128_bit_6 X128_bit_5 -X128_bit_4 -X128_bit_3 -X128_bit_2 X128_bit_1 -X128_bit0 -X128_bit1 -X128_bit2 -X128_bit3 -X128_bit4 -X128_bit5 -X128_bit6 -X128_bit7 -X128_bit8 -X128_bit9 -X128_bit10 -X128_bit11 -X128_bit12 X129_bit_7 X129_bit_6 X129_bit_5 -X129_bit_4 -X129_bit_3 -X129_bit_2 X129_bit_1 X129_bit0 X129_bit1 -X129_bit2 -X129_bit3 -X129_bit4 -X129_bit5 -X129_bit6 -X129_bit7 -X129_bit8 -X129_bit9 -X129_bit10 -X129_bit11 -X129_bit12 X130_bit_7 -X130_bit_6 -X130_bit_5 -X130_bit_4 -X130_bit_3 -X130_bit_2 -X130_bit_1 -X130_bit0 -X130_bit1 -X130_bit2 -X130_bit3 -X130_bit4 -X130_bit5 -X130_bit6 -X130_bit7 -X130_bit8 -X130_bit9 -X130_bit10 -X130_bit11 -X130_bit12 X131_bit_7 X131_bit_6 X131_bit_5 -X131_bit_4 -X131_bit_3 -X131_bit_2 -X131_bit_1 X131_bit0 -X131_bit1 -X131_bit2 -X131_bit3 -X131_bit4 -X131_bit5 -X131_bit6 -X131_bit7 -X131_bit8 -X131_bit9 -X131_bit10 -X131_bit11 -X131_bit12 X132_bit_7 X132_bit_6 X132_bit_5 -X132_bit_4 -X132_bit_3 -X132_bit_2 -X132_bit_1 -X132_bit0 -X132_bit1 -X132_bit2 -X132_bit3 -X132_bit4 -X132_bit5 -X132_bit6 -X132_bit7 -X132_bit8 -X132_bit9 -X132_bit10 -X132_bit11 -X132_bit12 -X133_bit_7 -X133_bit_6 -X133_bit_5 -X133_bit_4 -X133_bit_3 -X133_bit_2 -X133_bit_1 -X133_bit0 -X133_bit1 -X133_bit2 -X133_bit3 -X133_bit4 -X133_bit5 -X133_bit6 -X133_bit7 -X133_bit8 -X133_bit9 -X133_bit10 -X133_bit11 -X133_bit12 -X134_bit_7 -X134_bit_6 X134_bit_5 -X134_bit_4 -X134_bit_3 X134_bit_2 -X134_bit_1 X134_bit0 -X134_bit1 -X134_bit2 -X134_bit3 -X134_bit4 -X134_bit5 -X134_bit6 -X134_bit7 -X134_bit8 -X134_bit9 -X134_bit10 -X134_bit11 -X134_bit12 -X135_bit_7 -X135_bit_6 -X135_bit_5 -X135_bit_4 -X135_bit_3 -X135_bit_2 -X135_bit_1 -X135_bit0 -X135_bit1 -X135_bit2 -X135_bit3 -X135_bit4 -X135_bit5 -X135_bit6 -X135_bit7 -X135_bit8 -X135_bit9 -X135_bit10 -X135_bit11 -X135_bit12 X136_bit_7 X136_bit_6 X136_bit_5 -X136_bit_4 -X136_bit_3 X136_bit_2 -X136_bit_1 -X136_bit0 -X136_bit1 -X136_bit2 -X136_bit3 -X136_bit4 -X136_bit5 -X136_bit6 -X136_bit7 -X136_bit8 -X136_bit9 -X136_bit10 -X136_bit11 -X136_bit12 X137_bit_7 X137_bit_6 X137_bit_5 -X137_bit_4 -X137_bit_3 X137_bit_2 -X137_bit_1 X137_bit0 X137_bit1 -X137_bit2 -X137_bit3 -X137_bit4 -X137_bit5 -X137_bit6 -X137_bit7 -X137_bit8 -X137_bit9 -X137_bit10 -X137_bit11 -X137_bit12 X138_bit_7 -X138_bit_6 X138_bit_5 -X138_bit_4 -X138_bit_3 -X138_bit_2 -X138_bit_1 -X138_bit0 -X138_bit1 -X138_bit2 -X138_bit3 -X138_bit4 -X138_bit5 -X138_bit6 -X138_bit7 -X138_bit8 -X138_bit9 -X138_bit10 -X138_bit11 -X138_bit12 X139_bit_7 X139_bit_6 -X139_bit_5 -X139_bit_4 -X139_bit_3 X139_bit_2 -X139_bit_1 -X139_bit0 -X139_bit1 -X139_bit2 -X139_bit3 -X139_bit4 -X139_bit5 -X139_bit6 -X139_bit7 -X139_bit8 -X139_bit9 -X139_bit10 -X139_bit11 -X139_bit12 X140_bit_7 -X140_bit_6 X140_bit_5 -X140_bit_4 X140_bit_3 X140_bit_2 -X140_bit_1 -X140_bit0 X140_bit1 -X140_bit2 -X140_bit3 -X140_bit4 -X140_bit5 -X140_bit6 -X140_bit7 -X140_bit8 -X140_bit9 -X140_bit10 -X140_bit11 -X140_bit12 X141_bit_7 -X141_bit_6 X141_bit_5 -X141_bit_4 -X141_bit_3 -X141_bit_2 -X141_bit_1 -X141_bit0 -X141_bit1 -X141_bit2 -X141_bit3 -X141_bit4 -X141_bit5 -X141_bit6 -X141_bit7 -X141_bit8 -X141_bit9 -X141_bit10 -X141_bit11 -X141_bit12 X142_bit_7 X142_bit_6 X142_bit_5 X142_bit_4 -X142_bit_3 -X142_bit_2 -X142_bit_1 -X142_bit0 X142_bit1 -X142_bit2 -X142_bit3 -X142_bit4 -X142_bit5 -X142_bit6 -X142_bit7 -X142_bit8 -X142_bit9 -X142_bit10 -X142_bit11 -X142_bit12 -X143_bit_7 -X143_bit_6 -X143_bit_5 -X143_bit_4 -X143_bit_3 -X143_bit_2 -X143_bit_1 -X143_bit0 -X143_bit1 -X143_bit2 -X143_bit3 -X143_bit4 -X143_bit5 -X143_bit6 -X143_bit7 -X143_bit8 -X143_bit9 -X143_bit10 -X143_bit11 -X143_bit12 -X144_bit_7 -X144_bit_6 -X144_bit_5 -X144_bit_4 -X144_bit_3 -X144_bit_2 -X144_bit_1 -X144_bit0 -X144_bit1 -X144_bit2 -X144_bit3 -X144_bit4 -X144_bit5 -X144_bit6 -X144_bit7 -X144_bit8 -X144_bit9 -X144_bit10 -X144_bit11 -X144_bit12 -X145_bit_7 X145_bit_6 X145_bit_5 -X145_bit_4 X145_bit_3 X145_bit_2 -X145_bit_1 X145_bit0 -X145_bit1 X145_bit2 -X145_bit3 -X145_bit4 -X145_bit5 -X145_bit6 -X145_bit7 -X145_bit8 -X145_bit9 -X145_bit10 -X145_bit11 -X145_bit12 X146_bit_7 X146_bit_6 X146_bit_5 -X146_bit_4 -X146_bit_3 -X146_bit_2 -X146_bit_1 -X146_bit0 -X146_bit1 -X146_bit2 -X146_bit3 -X146_bit4 -X146_bit5 -X146_bit6 -X146_bit7 -X146_bit8 -X146_bit9 -X146_bit10 -X146_bit11 -X146_bit12 -X147_bit_7 X147_bit_6 -X147_bit_5 X147_bit_4 X147_bit_3 X147_bit_2 -X147_bit_1 -X147_bit0 X147_bit1 -X147_bit2 -X147_bit3 -X147_bit4 -X147_bit5 -X147_bit6 -X147_bit7 -X147_bit8 -X147_bit9 -X147_bit10 -X147_bit11 -X147_bit12 X148_bit_7 X148_bit_6 -X148_bit_5 -X148_bit_4 -X148_bit_3 -X148_bit_2 -X148_bit_1 -X148_bit0 -X148_bit1 -X148_bit2 -X148_bit3 -X148_bit4 -X148_bit5 -X148_bit6 -X148_bit7 -X148_bit8 -X148_bit9 -X148_bit10 -X148_bit11 -X148_bit12 -X149_bit_7 -X149_bit_6 -X149_bit_5 -X149_bit_4 -X149_bit_3 -X149_bit_2 -X149_bit_1 -X149_bit0 -X149_bit1 -X149_bit2 -X149_bit3 -X149_bit4 -X149_bit5 -X149_bit6 -X149_bit7 -X149_bit8 -X149_bit9 -X149_bit10 -X149_bit11 -X149_bit12 -X150_bit_7 -X150_bit_6 -X150_bit_5 -X150_bit_4 -X150_bit_3 -X150_bit_2 -X150_bit_1 -X150_bit0 -X150_bit1 -X150_bit2 -X150_bit3 -X150_bit4 -X150_bit5 -X150_bit6 -X150_bit7 -X150_bit8 -X150_bit9 -X150_bit10 -X150_bit11 -X150_bit12 X151_bit_7 -X151_bit_6 -X151_bit_5 -X151_bit_4 X151_bit_3 -X151_bit_2 X151_bit_1 X151_bit0 -X151_bit1 -X151_bit2 -X151_bit3 -X151_bit4 -X151_bit5 -X151_bit6 -X151_bit7 -X151_bit8 -X151_bit9 -X151_bit10 -X151_bit11 -X151_bit12 -X152_bit_7 -X152_bit_6 -X152_bit_5 -X152_bit_4 X152_bit_3 -X152_bit_2 -X152_bit_1 -X152_bit0 -X152_bit1 -X152_bit2 -X152_bit3 -X152_bit4 -X152_bit5 -X152_bit6 -X152_bit7 -X152_bit8 -X152_bit9 -X152_bit10 -X152_bit11 -X152_bit12 -X153_bit_7 -X153_bit_6 -X153_bit_5 -X153_bit_4 -X153_bit_3 -X153_bit_2 -X153_bit_1 -X153_bit0 -X153_bit1 -X153_bit2 -X153_bit3 -X153_bit4 -X153_bit5 -X153_bit6 -X153_bit7 -X153_bit8 -X153_bit9 -X153_bit10 -X153_bit11 -X153_bit12 -X154_bit_7 -X154_bit_6 -X154_bit_5 -X154_bit_4 -X154_bit_3 -X154_bit_2 -X154_bit_1 -X154_bit0 -X154_bit1 -X154_bit2 -X154_bit3 -X154_bit4 -X154_bit5 -X154_bit6 -X154_bit7 -X154_bit8 -X154_bit9 -X154_bit10 -X154_bit11 -X154_bit12 X155_bit_7 X155_bit_6 -X155_bit_5 -X155_bit_4 -X155_bit_3 -X155_bit_2 -X155_bit_1 X155_bit0 X155_bit1 X155_bit2 -X155_bit3 -X155_bit4 -X155_bit5 -X155_bit6 -X155_bit7 -X155_bit8 -X155_bit9 -X155_bit10 -X155_bit11 -X155_bit12 -X156_bit_7 -X156_bit_6 -X156_bit_5 -X156_bit_4 -X156_bit_3 -X156_bit_2 -X156_bit_1 -X156_bit0 -X156_bit1 -X156_bit2 -X156_bit3 -X156_bit4 -X156_bit5 -X156_bit6 -X156_bit7 -X156_bit8 -X156_bit9 -X156_bit10 -X156_bit11 -X156_bit12 X157_bit_7 X157_bit_6 X157_bit_5 -X157_bit_4 -X157_bit_3 -X157_bit_2 -X157_bit_1 -X157_bit0 -X157_bit1 -X157_bit2 -X157_bit3 -X157_bit4 -X157_bit5 -X157_bit6 -X157_bit7 -X157_bit8 -X157_bit9 -X157_bit10 -X157_bit11 -X157_bit12 -X158_bit_7 -X158_bit_6 -X158_bit_5 -X158_bit_4 -X158_bit_3 -X158_bit_2 -X158_bit_1 -X158_bit0 -X158_bit1 -X158_bit2 -X158_bit3 -X158_bit4 -X158_bit5 -X158_bit6 -X158_bit7 -X158_bit8 -X158_bit9 -X158_bit10 -X158_bit11 -X158_bit12 X159_bit_7 X159_bit_6 -X159_bit_5 X159_bit_4 X159_bit_3 -X159_bit_2 -X159_bit_1 X159_bit0 -X159_bit1 -X159_bit2 -X159_bit3 -X159_bit4 -X159_bit5 -X159_bit6 -X159_bit7 -X159_bit8 -X159_bit9 -X159_bit10 -X159_bit11 -X159_bit12 X160_bit_7 -X160_bit_6 -X160_bit_5 X160_bit_4 -X160_bit_3 -X160_bit_2 -X160_bit_1 X160_bit0 X160_bit1 -X160_bit2 -X160_bit3 -X160_bit4 -X160_bit5 -X160_bit6 -X160_bit7 -X160_bit8 -X160_bit9 -X160_bit10 -X160_bit11 -X160_bit12 X161_bit_7 -X161_bit_6 -X161_bit_5 X161_bit_4 X161_bit_3 -X161_bit_2 -X161_bit_1 X161_bit0 X161_bit1 X161_bit2 -X161_bit3 -X161_bit4 -X161_bit5 -X161_bit6 -X161_bit7 -X161_bit8 -X161_bit9 -X161_bit10 -X161_bit11 -X161_bit12 -X162_bit_7 -X162_bit_6 -X162_bit_5 -X162_bit_4 -X162_bit_3 -X162_bit_2 -X162_bit_1 -X162_bit0 -X162_bit1 -X162_bit2 -X162_bit3 -X162_bit4 -X162_bit5 -X162_bit6 -X162_bit7 -X162_bit8 -X162_bit9 -X162_bit10 -X162_bit11 -X162_bit12 -X163_bit_7 -X163_bit_6 -X163_bit_5 -X163_bit_4 -X163_bit_3 -X163_bit_2 -X163_bit_1 -X163_bit0 -X163_bit1 -X163_bit2 -X163_bit3 -X163_bit4 -X163_bit5 -X163_bit6 -X163_bit7 -X163_bit8 -X163_bit9 -X163_bit10 -X163_bit11 -X163_bit12 X164_bit_7 -X164_bit_6 -X164_bit_5 -X164_bit_4 -X164_bit_3 -X164_bit_2 -X164_bit_1 -X164_bit0 -X164_bit1 -X164_bit2 -X164_bit3 -X164_bit4 -X164_bit5 -X164_bit6 -X164_bit7 -X164_bit8 -X164_bit9 -X164_bit10 -X164_bit11 -X164_bit12 -X165_bit_7 -X165_bit_6 -X165_bit_5 -X165_bit_4 -X165_bit_3 -X165_bit_2 -X165_bit_1 -X165_bit0 -X165_bit1 -X165_bit2 -X165_bit3 -X165_bit4 -X165_bit5 -X165_bit6 -X165_bit7 -X165_bit8 -X165_bit9 -X165_bit10 -X165_bit11 -X165_bit12 -X166_bit_7 -X166_bit_6 -X166_bit_5 -X166_bit_4 -X166_bit_3 -X166_bit_2 -X166_bit_1 -X166_bit0 -X166_bit1 -X166_bit2 -X166_bit3 -X166_bit4 -X166_bit5 -X166_bit6 -X166_bit7 -X166_bit8 -X166_bit9 -X166_bit10 -X166_bit11 -X166_bit12 X167_bit_7 X167_bit_6 -X167_bit_5 -X167_bit_4 -X167_bit_3 X167_bit_2 X167_bit_1 X167_bit0 -X167_bit1 -X167_bit2 -X167_bit3 -X167_bit4 -X167_bit5 -X167_bit6 -X167_bit7 -X167_bit8 -X167_bit9 -X167_bit10 -X167_bit11 -X167_bit12 -X168_bit_7 X168_bit_6 -X168_bit_5 -X168_bit_4 -X168_bit_3 -X168_bit_2 -X168_bit_1 -X168_bit0 -X168_bit1 -X168_bit2 -X168_bit3 -X168_bit4 -X168_bit5 -X168_bit6 -X168_bit7 -X168_bit8 -X168_bit9 -X168_bit10 -X168_bit11 -X168_bit12 -X169_bit_7 -X169_bit_6 -X169_bit_5 -X169_bit_4 -X169_bit_3 -X169_bit_2 -X169_bit_1 -X169_bit0 -X169_bit1 -X169_bit2 -X169_bit3 -X169_bit4 -X169_bit5 -X169_bit6 -X169_bit7 -X169_bit8 -X169_bit9 -X169_bit10 -X169_bit11 -X169_bit12 -X170_bit_7 -X170_bit_6 -X170_bit_5 -X170_bit_4 -X170_bit_3 -X170_bit_2 -X170_bit_1 -X170_bit0 -X170_bit1 -X170_bit2 -X170_bit3 -X170_bit4 -X170_bit5 -X170_bit6 -X170_bit7 -X170_bit8 -X170_bit9 -X170_bit10 -X170_bit11 -X170_bit12 -X171_bit_7 -X171_bit_6 -X171_bit_5 -X171_bit_4 -X171_bit_3 -X171_bit_2 -X171_bit_1 -X171_bit0 -X171_bit1 -X171_bit2 -X171_bit3 -X171_bit4 -X171_bit5 -X171_bit6 -X171_bit7 -X171_bit8 -X171_bit9 -X171_bit10 -X171_bit11 -X171_bit12 -X172_bit_7 -X172_bit_6 -X172_bit_5 -X172_bit_4 -X172_bit_3 -X172_bit_2 -X172_bit_1 -X172_bit0 -X172_bit1 -X172_bit2 -X172_bit3 -X172_bit4 -X172_bit5 -X172_bit6 -X172_bit7 -X172_bit8 -X172_bit9 -X172_bit10 -X172_bit11 -X172_bit12 -X173_bit_7 X173_bit_6 -X173_bit_5 -X173_bit_4 -X173_bit_3 -X173_bit_2 -X173_bit_1 -X173_bit0 -X173_bit1 -X173_bit2 -X173_bit3 -X173_bit4 -X173_bit5 -X173_bit6 -X173_bit7 -X173_bit8 -X173_bit9 -X173_bit10 -X173_bit11 -X173_bit12 -X174_bit_7 -X174_bit_6 -X174_bit_5 -X174_bit_4 -X174_bit_3 -X174_bit_2 -X174_bit_1 -X174_bit0 -X174_bit1 -X174_bit2 -X174_bit3 -X174_bit4 -X174_bit5 -X174_bit6 -X174_bit7 -X174_bit8 -X174_bit9 -X174_bit10 -X174_bit11 -X174_bit12 -X175_bit_7 X175_bit_6 X175_bit_5 -X175_bit_4 X175_bit_3 X175_bit_2 X175_bit_1 -X175_bit0 X175_bit1 X175_bit2 -X175_bit3 -X175_bit4 -X175_bit5 -X175_bit6 -X175_bit7 -X175_bit8 -X175_bit9 -X175_bit10 -X175_bit11 -X175_bit12 -X176_bit_7 -X176_bit_6 -X176_bit_5 X176_bit_4 -X176_bit_3 X176_bit_2 X176_bit_1 -X176_bit0 -X176_bit1 -X176_bit2 -X176_bit3 -X176_bit4 -X176_bit5 -X176_bit6 -X176_bit7 -X176_bit8 -X176_bit9 -X176_bit10 -X176_bit11 -X176_bit12 -X177_bit_7 -X177_bit_6 -X177_bit_5 -X177_bit_4 -X177_bit_3 -X177_bit_2 -X177_bit_1 -X177_bit0 -X177_bit1 -X177_bit2 -X177_bit3 -X177_bit4 -X177_bit5 -X177_bit6 -X177_bit7 -X177_bit8 -X177_bit9 -X177_bit10 -X177_bit11 -X177_bit12 X178_bit_7 -X178_bit_6 X178_bit_5 X178_bit_4 -X178_bit_3 -X178_bit_2 -X178_bit_1 X178_bit0 -X178_bit1 -X178_bit2 -X178_bit3 -X178_bit4 -X178_bit5 -X178_bit6 -X178_bit7 -X178_bit8 -X178_bit9 -X178_bit10 -X178_bit11 -X178_bit12 -X179_bit_7 -X179_bit_6 X179_bit_5 X179_bit_4 -X179_bit_3 X179_bit_2 -X179_bit_1 X179_bit0 X179_bit1 -X179_bit2 X179_bit3 -X179_bit4 -X179_bit5 -X179_bit6 -X179_bit7 -X179_bit8 -X179_bit9 -X179_bit10 -X179_bit11 -X179_bit12 X180_bit_7 X180_bit_6 -X180_bit_5 -X180_bit_4 -X180_bit_3 -X180_bit_2 -X180_bit_1 -X180_bit0 -X180_bit1 -X180_bit2 -X180_bit3 -X180_bit4 -X180_bit5 -X180_bit6 -X180_bit7 -X180_bit8 -X180_bit9 -X180_bit10 -X180_bit11 -X180_bit12 -X181_bit_7 X181_bit_6 X181_bit_5 X181_bit_4 -X181_bit_3 X181_bit_2 X181_bit_1 -X181_bit0 X181_bit1 -X181_bit2 -X181_bit3 -X181_bit4 -X181_bit5 -X181_bit6 -X181_bit7 -X181_bit8 -X181_bit9 -X181_bit10 -X181_bit11 -X181_bit12 X182_bit_7 -X182_bit_6 -X182_bit_5 -X182_bit_4 X182_bit_3 X182_bit_2 X182_bit_1 -X182_bit0 -X182_bit1 X182_bit2 X182_bit3 -X182_bit4 -X182_bit5 -X182_bit6 -X182_bit7 -X182_bit8 -X182_bit9 -X182_bit10 -X182_bit11 -X182_bit12 -X183_bit_7 -X183_bit_6 -X183_bit_5 -X183_bit_4 -X183_bit_3 -X183_bit_2 -X183_bit_1 -X183_bit0 -X183_bit1 -X183_bit2 -X183_bit3 -X183_bit4 -X183_bit5 -X183_bit6 -X183_bit7 -X183_bit8 -X183_bit9 -X183_bit10 -X183_bit11 -X183_bit12 -X184_bit_7 X184_bit_6 -X184_bit_5 -X184_bit_4 X184_bit_3 -X184_bit_2 -X184_bit_1 -X184_bit0 -X184_bit1 -X184_bit2 -X184_bit3 -X184_bit4 -X184_bit5 -X184_bit6 -X184_bit7 -X184_bit8 -X184_bit9 -X184_bit10 -X184_bit11 -X184_bit12 -X185_bit_7 -X185_bit_6 -X185_bit_5 -X185_bit_4 -X185_bit_3 -X185_bit_2 -X185_bit_1 -X185_bit0 -X185_bit1 -X185_bit2 -X185_bit3 -X185_bit4 -X185_bit5 -X185_bit6 -X185_bit7 -X185_bit8 -X185_bit9 -X185_bit10 -X185_bit11 -X185_bit12 -X186_bit_7 -X186_bit_6 -X186_bit_5 -X186_bit_4 -X186_bit_3 -X186_bit_2 -X186_bit_1 -X186_bit0 -X186_bit1 -X186_bit2 -X186_bit3 -X186_bit4 -X186_bit5 -X186_bit6 -X186_bit7 -X186_bit8 -X186_bit9 -X186_bit10 -X186_bit11 -X186_bit12 X187_bit_7 -X187_bit_6 X187_bit_5 X187_bit_4 -X187_bit_3 X187_bit_2 X187_bit_1 -X187_bit0 X187_bit1 X187_bit2 -X187_bit3 -X187_bit4 -X187_bit5 -X187_bit6 -X187_bit7 -X187_bit8 -X187_bit9 -X187_bit10 -X187_bit11 -X187_bit12 -X188_bit_7 -X188_bit_6 -X188_bit_5 -X188_bit_4 -X188_bit_3 -X188_bit_2 -X188_bit_1 -X188_bit0 -X188_bit1 -X188_bit2 -X188_bit3 -X188_bit4 -X188_bit5 -X188_bit6 -X188_bit7 -X188_bit8 -X188_bit9 -X188_bit10 -X188_bit11 -X188_bit12 X189_bit_7 -X189_bit_6 -X189_bit_5 -X189_bit_4 -X189_bit_3 -X189_bit_2 -X189_bit_1 -X189_bit0 -X189_bit1 -X189_bit2 -X189_bit3 -X189_bit4 -X189_bit5 -X189_bit6 -X189_bit7 -X189_bit8 -X189_bit9 -X189_bit10 -X189_bit11 -X189_bit12 -X190_bit_7 -X190_bit_6 -X190_bit_5 -X190_bit_4 -X190_bit_3 -X190_bit_2 -X190_bit_1 -X190_bit0 -X190_bit1 -X190_bit2 -X190_bit3 -X190_bit4 -X190_bit5 -X190_bit6 -X190_bit7 -X190_bit8 -X190_bit9 -X190_bit10 -X190_bit11 -X190_bit12 X191_bit_7 -X191_bit_6 X191_bit_5 X191_bit_4 X191_bit_3 X191_bit_2 X191_bit_1 X191_bit0 -X191_bit1 -X191_bit2 -X191_bit3 -X191_bit4 -X191_bit5 -X191_bit6 -X191_bit7 -X191_bit8 -X191_bit9 -X191_bit10 -X191_bit11 -X191_bit12 X192_bit_7 X192_bit_6 X192_bit_5 X192_bit_4 X192_bit_3 -X192_bit_2 -X192_bit_1 -X192_bit0 -X192_bit1 -X192_bit2 -X192_bit3 -X192_bit4 -X192_bit5 -X192_bit6 -X192_bit7 -X192_bit8 -X192_bit9 -X192_bit10 -X192_bit11 -X192_bit12 -X193_bit_7 -X193_bit_6 X193_bit_5 X193_bit_4 -X193_bit_3 -X193_bit_2 -X193_bit_1 -X193_bit0 -X193_bit1 -X193_bit2 -X193_bit3 -X193_bit4 -X193_bit5 -X193_bit6 -X193_bit7 -X193_bit8 -X193_bit9 -X193_bit10 -X193_bit11 -X193_bit12 -X194_bit_7 X194_bit_6 -X194_bit_5 -X194_bit_4 -X194_bit_3 -X194_bit_2 -X194_bit_1 -X194_bit0 -X194_bit1 -X194_bit2 -X194_bit3 -X194_bit4 -X194_bit5 -X194_bit6 -X194_bit7 -X194_bit8 -X194_bit9 -X194_bit10 -X194_bit11 -X194_bit12 X195_bit_7 X195_bit_6 X195_bit_5 X195_bit_4 X195_bit_3 -X195_bit_2 X195_bit_1 X195_bit0 -X195_bit1 -X195_bit2 -X195_bit3 -X195_bit4 -X195_bit5 -X195_bit6 -X195_bit7 -X195_bit8 -X195_bit9 -X195_bit10 -X195_bit11 -X195_bit12 -X196_bit_7 -X196_bit_6 -X196_bit_5 -X196_bit_4 -X196_bit_3 -X196_bit_2 -X196_bit_1 -X196_bit0 -X196_bit1 -X196_bit2 -X196_bit3 -X196_bit4 -X196_bit5 -X196_bit6 -X196_bit7 -X196_bit8 -X196_bit9 -X196_bit10 -X196_bit11 -X196_bit12 -X197_bit_7 X197_bit_6 X197_bit_5 X197_bit_4 X197_bit_3 -X197_bit_2 X197_bit_1 -X197_bit0 -X197_bit1 -X197_bit2 -X197_bit3 -X197_bit4 -X197_bit5 -X197_bit6 -X197_bit7 -X197_bit8 -X197_bit9 -X197_bit10 -X197_bit11 -X197_bit12 X198_bit_7 X198_bit_6 X198_bit_5 X198_bit_4 -X198_bit_3 X198_bit_2 X198_bit_1 -X198_bit0 -X198_bit1 -X198_bit2 -X198_bit3 -X198_bit4 -X198_bit5 -X198_bit6 -X198_bit7 -X198_bit8 -X198_bit9 -X198_bit10 -X198_bit11 -X198_bit12 X199_bit_7 X199_bit_6 X199_bit_5 X199_bit_4 X199_bit_3 X199_bit_2 X199_bit_1 -X199_bit0 -X199_bit1 -X199_bit2 -X199_bit3 -X199_bit4 -X199_bit5 -X199_bit6 -X199_bit7 -X199_bit8 -X199_bit9 -X199_bit10 -X199_bit11 -X199_bit12 X200_bit_7 -X200_bit_6 -X200_bit_5 -X200_bit_4 -X200_bit_3 -X200_bit_2 -X200_bit_1 -X200_bit0 -X200_bit1 -X200_bit2 -X200_bit3 -X200_bit4 -X200_bit5 -X200_bit6 -X200_bit7 -X200_bit8 -X200_bit9 -X200_bit10 -X200_bit11 -X200_bit12 -X201_bit_7 -X201_bit_6 -X201_bit_5 -X201_bit_4 -X201_bit_3 -X201_bit_2 -X201_bit_1 -X201_bit0 -X201_bit1 -X201_bit2 -X201_bit3 -X201_bit4 -X201_bit5 -X201_bit6 -X201_bit7 -X201_bit8 -X201_bit9 -X201_bit10 -X201_bit11 -X201_bit12 X202_bit_7 X202_bit_6 X202_bit_5 -X202_bit_4 -X202_bit_3 -X202_bit_2 -X202_bit_1 -X202_bit0 -X202_bit1 -X202_bit2 -X202_bit3 -X202_bit4 -X202_bit5 -X202_bit6 -X202_bit7 -X202_bit8 -X202_bit9 -X202_bit10 -X202_bit11 -X202_bit12 -X203_bit_7 -X203_bit_6 -X203_bit_5 -X203_bit_4 -X203_bit_3 -X203_bit_2 -X203_bit_1 -X203_bit0 -X203_bit1 -X203_bit2 -X203_bit3 -X203_bit4 -X203_bit5 -X203_bit6 -X203_bit7 -X203_bit8 -X203_bit9 -X203_bit10 -X203_bit11 -X203_bit12 -X204_bit_7 -X204_bit_6 -X204_bit_5 -X204_bit_4 -X204_bit_3 -X204_bit_2 -X204_bit_1 -X204_bit0 -X204_bit1 -X204_bit2 -X204_bit3 -X204_bit4 -X204_bit5 -X204_bit6 -X204_bit7 -X204_bit8 -X204_bit9 -X204_bit10 -X204_bit11 -X204_bit12 X205_bit_7 X205_bit_6 X205_bit_5 X205_bit_4 -X205_bit_3 -X205_bit_2 -X205_bit_1 -X205_bit0 -X205_bit1 -X205_bit2 -X205_bit3 -X205_bit4 -X205_bit5 -X205_bit6 -X205_bit7 -X205_bit8 -X205_bit9 -X205_bit10 -X205_bit11 -X205_bit12 X206_bit_7 -X206_bit_6 X206_bit_5 X206_bit_4 X206_bit_3 -X206_bit_2 X206_bit_1 -X206_bit0 -X206_bit1 -X206_bit2 -X206_bit3 -X206_bit4 -X206_bit5 -X206_bit6 -X206_bit7 -X206_bit8 -X206_bit9 -X206_bit10 -X206_bit11 -X206_bit12 -X207_bit_7 -X207_bit_6 X207_bit_5 -X207_bit_4 X207_bit_3 X207_bit_2 -X207_bit_1 -X207_bit0 -X207_bit1 -X207_bit2 -X207_bit3 -X207_bit4 -X207_bit5 -X207_bit6 -X207_bit7 -X207_bit8 -X207_bit9 -X207_bit10 -X207_bit11 -X207_bit12 X208_bit_7 -X208_bit_6 X208_bit_5 -X208_bit_4 -X208_bit_3 X208_bit_2 -X208_bit_1 X208_bit0 -X208_bit1 -X208_bit2 -X208_bit3 -X208_bit4 -X208_bit5 -X208_bit6 -X208_bit7 -X208_bit8 -X208_bit9 -X208_bit10 -X208_bit11 -X208_bit12 -X209_bit_7 -X209_bit_6 -X209_bit_5 -X209_bit_4 -X209_bit_3 -X209_bit_2 -X209_bit_1 -X209_bit0 -X209_bit1 -X209_bit2 -X209_bit3 -X209_bit4 -X209_bit5 -X209_bit6 -X209_bit7 -X209_bit8 -X209_bit9 -X209_bit10 -X209_bit11 -X209_bit12 -X210_bit_7 -X210_bit_6 -X210_bit_5 -X210_bit_4 -X210_bit_3 -X210_bit_2 -X210_bit_1 -X210_bit0 -X210_bit1 -X210_bit2 -X210_bit3 -X210_bit4 -X210_bit5 -X210_bit6 -X210_bit7 -X210_bit8 -X210_bit9 -X210_bit10 -X210_bit11 -X210_bit12 -X211_bit_7 X211_bit_6 X211_bit_5 X211_bit_4 -X211_bit_3 -X211_bit_2 -X211_bit_1 X211_bit0 -X211_bit1 X211_bit2 -X211_bit3 -X211_bit4 -X211_bit5 -X211_bit6 -X211_bit7 -X211_bit8 -X211_bit9 -X211_bit10 -X211_bit11 -X211_bit12 X212_bit_7 X212_bit_6 -X212_bit_5 -X212_bit_4 -X212_bit_3 -X212_bit_2 -X212_bit_1 -X212_bit0 -X212_bit1 -X212_bit2 -X212_bit3 -X212_bit4 -X212_bit5 -X212_bit6 -X212_bit7 -X212_bit8 -X212_bit9 -X212_bit10 -X212_bit11 -X212_bit12 -X213_bit_7 -X213_bit_6 -X213_bit_5 -X213_bit_4 -X213_bit_3 -X213_bit_2 -X213_bit_1 -X213_bit0 -X213_bit1 -X213_bit2 -X213_bit3 -X213_bit4 -X213_bit5 -X213_bit6 -X213_bit7 -X213_bit8 -X213_bit9 -X213_bit10 -X213_bit11 -X213_bit12 -X214_bit_7 -X214_bit_6 -X214_bit_5 -X214_bit_4 -X214_bit_3 -X214_bit_2 -X214_bit_1 -X214_bit0 -X214_bit1 -X214_bit2 -X214_bit3 -X214_bit4 -X214_bit5 -X214_bit6 -X214_bit7 -X214_bit8 -X214_bit9 -X214_bit10 -X214_bit11 -X214_bit12 X215_bit_7 X215_bit_6 X215_bit_5 -X215_bit_4 X215_bit_3 X215_bit_2 X215_bit_1 -X215_bit0 -X215_bit1 -X215_bit2 -X215_bit3 -X215_bit4 -X215_bit5 -X215_bit6 -X215_bit7 -X215_bit8 -X215_bit9 -X215_bit10 -X215_bit11 -X215_bit12 -X216_bit_7 -X216_bit_6 X216_bit_5 -X216_bit_4 X216_bit_3 -X216_bit_2 -X216_bit_1 -X216_bit0 -X216_bit1 X216_bit2 -X216_bit3 -X216_bit4 -X216_bit5 -X216_bit6 -X216_bit7 -X216_bit8 -X216_bit9 -X216_bit10 -X216_bit11 -X216_bit12 X217_bit_7 -X217_bit_6 X217_bit_5 -X217_bit_4 X217_bit_3 X217_bit_2 -X217_bit_1 X217_bit0 -X217_bit1 -X217_bit2 -X217_bit3 -X217_bit4 -X217_bit5 -X217_bit6 -X217_bit7 -X217_bit8 -X217_bit9 -X217_bit10 -X217_bit11 -X217_bit12 -X218_bit_7 -X218_bit_6 X218_bit_5 -X218_bit_4 -X218_bit_3 -X218_bit_2 -X218_bit_1 -X218_bit0 -X218_bit1 -X218_bit2 -X218_bit3 -X218_bit4 -X218_bit5 -X218_bit6 -X218_bit7 -X218_bit8 -X218_bit9 -X218_bit10 -X218_bit11 -X218_bit12 -X219_bit_7 -X219_bit_6 -X219_bit_5 -X219_bit_4 -X219_bit_3 -X219_bit_2 -X219_bit_1 -X219_bit0 -X219_bit1 -X219_bit2 -X219_bit3 -X219_bit4 -X219_bit5 -X219_bit6 -X219_bit7 -X219_bit8 -X219_bit9 -X219_bit10 -X219_bit11 -X219_bit12 -X220_bit_7 -X220_bit_6 -X220_bit_5 -X220_bit_4 -X220_bit_3 -X220_bit_2 -X220_bit_1 -X220_bit0 -X220_bit1 -X220_bit2 -X220_bit3 -X220_bit4 -X220_bit5 -X220_bit6 -X220_bit7 -X220_bit8 -X220_bit9 -X220_bit10 -X220_bit11 -X220_bit12 -X221_bit_7 X221_bit_6 X221_bit_5 -X221_bit_4 -X221_bit_3 -X221_bit_2 -X221_bit_1 -X221_bit0 -X221_bit1 -X221_bit2 -X221_bit3 -X221_bit4 -X221_bit5 -X221_bit6 -X221_bit7 -X221_bit8 -X221_bit9 -X221_bit10 -X221_bit11 -X221_bit12 -X222_bit_7 -X222_bit_6 -X222_bit_5 -X222_bit_4 -X222_bit_3 -X222_bit_2 -X222_bit_1 -X222_bit0 -X222_bit1 -X222_bit2 -X222_bit3 -X222_bit4 -X222_bit5 -X222_bit6 -X222_bit7 -X222_bit8 -X222_bit9 -X222_bit10 -X222_bit11 -X222_bit12 -X223_bit_7 -X223_bit_6 -X223_bit_5 -X223_bit_4 -X223_bit_3 -X223_bit_2 -X223_bit_1 -X223_bit0 -X223_bit1 -X223_bit2 -X223_bit3 -X223_bit4 -X223_bit5 -X223_bit6 -X223_bit7 -X223_bit8 -X223_bit9 -X223_bit10 -X223_bit11 -X223_bit12 X224_bit_7 -X224_bit_6 -X224_bit_5 -X224_bit_4 -X224_bit_3 X224_bit_2 X224_bit_1 -X224_bit0 -X224_bit1 -X224_bit2 -X224_bit3 -X224_bit4 -X224_bit5 -X224_bit6 -X224_bit7 -X224_bit8 -X224_bit9 -X224_bit10 -X224_bit11 -X224_bit12 -X225_bit_7 -X225_bit_6 -X225_bit_5 -X225_bit_4 -X225_bit_3 -X225_bit_2 -X225_bit_1 -X225_bit0 -X225_bit1 -X225_bit2 -X225_bit3 -X225_bit4 -X225_bit5 -X225_bit6 -X225_bit7 -X225_bit8 -X225_bit9 -X225_bit10 -X225_bit11 -X225_bit12 -X226_bit_7 X226_bit_6 -X226_bit_5 -X226_bit_4 -X226_bit_3 -X226_bit_2 -X226_bit_1 -X226_bit0 -X226_bit1 -X226_bit2 -X226_bit3 -X226_bit4 -X226_bit5 -X226_bit6 -X226_bit7 -X226_bit8 -X226_bit9 -X226_bit10 -X226_bit11 -X226_bit12 -X227_bit_7 -X227_bit_6 -X227_bit_5 -X227_bit_4 -X227_bit_3 -X227_bit_2 -X227_bit_1 -X227_bit0 -X227_bit1 -X227_bit2 -X227_bit3 -X227_bit4 -X227_bit5 -X227_bit6 -X227_bit7 -X227_bit8 -X227_bit9 -X227_bit10 -X227_bit11 -X227_bit12 -X228_bit_7 -X228_bit_6 -X228_bit_5 -X228_bit_4 -X228_bit_3 -X228_bit_2 -X228_bit_1 -X228_bit0 -X228_bit1 -X228_bit2 -X228_bit3 -X228_bit4 -X228_bit5 -X228_bit6 -X228_bit7 -X228_bit8 -X228_bit9 -X228_bit10 -X228_bit11 -X228_bit12 X229_bit_7 -X229_bit_6 X229_bit_5 -X229_bit_4 X229_bit_3 -X229_bit_2 -X229_bit_1 -X229_bit0 X229_bit1 -X229_bit2 -X229_bit3 -X229_bit4 -X229_bit5 -X229_bit6 -X229_bit7 -X229_bit8 -X229_bit9 -X229_bit10 -X229_bit11 -X229_bit12 -X230_bit_7 -X230_bit_6 -X230_bit_5 -X230_bit_4 X230_bit_3 -X230_bit_2 X230_bit_1 -X230_bit0 -X230_bit1 -X230_bit2 X230_bit3 X230_bit4 -X230_bit5 -X230_bit6 -X230_bit7 -X230_bit8 -X230_bit9 -X230_bit10 -X230_bit11 -X230_bit12 -X231_bit_7 -X231_bit_6 -X231_bit_5 -X231_bit_4 -X231_bit_3 -X231_bit_2 -X231_bit_1 -X231_bit0 -X231_bit1 -X231_bit2 -X231_bit3 -X231_bit4 -X231_bit5 -X231_bit6 -X231_bit7 -X231_bit8 -X231_bit9 -X231_bit10 -X231_bit11 -X231_bit12 X232_bit_7 -X232_bit_6 X232_bit_5 -X232_bit_4 X232_bit_3 -X232_bit_2 -X232_bit_1 -X232_bit0 -X232_bit1 -X232_bit2 -X232_bit3 -X232_bit4 -X232_bit5 -X232_bit6 -X232_bit7 -X232_bit8 -X232_bit9 -X232_bit10 -X232_bit11 -X232_bit12 X233_bit_7 X233_bit_6 X233_bit_5 X233_bit_4 -X233_bit_3 -X233_bit_2 -X233_bit_1 X233_bit0 -X233_bit1 -X233_bit2 -X233_bit3 -X233_bit4 -X233_bit5 -X233_bit6 -X233_bit7 -X233_bit8 -X233_bit9 -X233_bit10 -X233_bit11 -X233_bit12 -X234_bit_7 -X234_bit_6 -X234_bit_5 -X234_bit_4 -X234_bit_3 -X234_bit_2 -X234_bit_1 -X234_bit0 -X234_bit1 -X234_bit2 -X234_bit3 -X234_bit4 -X234_bit5 -X234_bit6 -X234_bit7 -X234_bit8 -X234_bit9 -X234_bit10 -X234_bit11 -X234_bit12 X235_bit_7 -X235_bit_6 X235_bit_5 -X235_bit_4 X235_bit_3 -X235_bit_2 X235_bit_1 -X235_bit0 -X235_bit1 -X235_bit2 X235_bit3 -X235_bit4 -X235_bit5 -X235_bit6 -X235_bit7 -X235_bit8 -X235_bit9 -X235_bit10 -X235_bit11 -X235_bit12 -X236_bit_7 -X236_bit_6 -X236_bit_5 -X236_bit_4 X236_bit_3 X236_bit_2 -X236_bit_1 -X236_bit0 -X236_bit1 -X236_bit2 -X236_bit3 -X236_bit4 -X236_bit5 -X236_bit6 -X236_bit7 -X236_bit8 -X236_bit9 -X236_bit10 -X236_bit11 -X236_bit12 X237_bit_7 X237_bit_6 X237_bit_5 X237_bit_4 -X237_bit_3 -X237_bit_2 -X237_bit_1 -X237_bit0 -X237_bit1 -X237_bit2 -X237_bit3 -X237_bit4 -X237_bit5 -X237_bit6 -X237_bit7 -X237_bit8 -X237_bit9 -X237_bit10 -X237_bit11 -X237_bit12 -X238_bit_7 -X238_bit_6 -X238_bit_5 -X238_bit_4 -X238_bit_3 -X238_bit_2 -X238_bit_1 -X238_bit0 -X238_bit1 -X238_bit2 -X238_bit3 -X238_bit4 -X238_bit5 -X238_bit6 -X238_bit7 -X238_bit8 -X238_bit9 -X238_bit10 -X238_bit11 -X238_bit12 -X239_bit_7 -X239_bit_6 -X239_bit_5 -X239_bit_4 -X239_bit_3 -X239_bit_2 -X239_bit_1 -X239_bit0 -X239_bit1 -X239_bit2 -X239_bit3 -X239_bit4 -X239_bit5 -X239_bit6 -X239_bit7 -X239_bit8 -X239_bit9 -X239_bit10 -X239_bit11 -X239_bit12 -X240_bit_7 -X240_bit_6 -X240_bit_5 -X240_bit_4 -X240_bit_3 -X240_bit_2 -X240_bit_1 -X240_bit0 -X240_bit1 -X240_bit2 -X240_bit3 -X240_bit4 -X240_bit5 -X240_bit6 -X240_bit7 -X240_bit8 -X240_bit9 -X240_bit10 -X240_bit11 -X240_bit12 X241_bit_7 X241_bit_6 -X241_bit_5 -X241_bit_4 -X241_bit_3 -X241_bit_2 -X241_bit_1 -X241_bit0 -X241_bit1 -X241_bit2 -X241_bit3 -X241_bit4 -X241_bit5 -X241_bit6 -X241_bit7 -X241_bit8 -X241_bit9 -X241_bit10 -X241_bit11 -X241_bit12 X242_bit_7 X242_bit_6 -X242_bit_5 -X242_bit_4 -X242_bit_3 -X242_bit_2 -X242_bit_1 -X242_bit0 -X242_bit1 -X242_bit2 -X242_bit3 -X242_bit4 -X242_bit5 -X242_bit6 -X242_bit7 -X242_bit8 -X242_bit9 -X242_bit10 -X242_bit11 -X242_bit12 -X243_bit_7 -X243_bit_6 -X243_bit_5 -X243_bit_4 X243_bit_3 X243_bit_2 -X243_bit_1 -X243_bit0 -X243_bit1 -X243_bit2 -X243_bit3 -X243_bit4 -X243_bit5 -X243_bit6 -X243_bit7 -X243_bit8 -X243_bit9 -X243_bit10 -X243_bit11 -X243_bit12 X244_bit_7 -X244_bit_6 -X244_bit_5 -X244_bit_4 X244_bit_3 -X244_bit_2 X244_bit_1 -X244_bit0 -X244_bit1 -X244_bit2 -X244_bit3 -X244_bit4 -X244_bit5 -X244_bit6 -X244_bit7 -X244_bit8 -X244_bit9 -X244_bit10 -X244_bit11 -X244_bit12 X245_bit_7 -X245_bit_6 -X245_bit_5 -X245_bit_4 X245_bit_3 X245_bit_2 X245_bit_1 -X245_bit0 -X245_bit1 -X245_bit2 -X245_bit3 -X245_bit4 -X245_bit5 -X245_bit6 -X245_bit7 -X245_bit8 -X245_bit9 -X245_bit10 -X245_bit11 -X245_bit12 -X246_bit_7 -X246_bit_6 -X246_bit_5 -X246_bit_4 -X246_bit_3 -X246_bit_2 -X246_bit_1 -X246_bit0 -X246_bit1 -X246_bit2 -X246_bit3 -X246_bit4 -X246_bit5 -X246_bit6 -X246_bit7 -X246_bit8 -X246_bit9 -X246_bit10 -X246_bit11 -X246_bit12 X247_bit_7 -X247_bit_6 -X247_bit_5 -X247_bit_4 X247_bit_3 -X247_bit_2 -X247_bit_1 -X247_bit0 -X247_bit1 -X247_bit2 -X247_bit3 -X247_bit4 -X247_bit5 -X247_bit6 -X247_bit7 -X247_bit8 -X247_bit9 -X247_bit10 -X247_bit11 -X247_bit12 -X248_bit_7 -X248_bit_6 -X248_bit_5 -X248_bit_4 X248_bit_3 -X248_bit_2 -X248_bit_1 -X248_bit0 -X248_bit1 -X248_bit2 -X248_bit3 -X248_bit4 -X248_bit5 -X248_bit6 -X248_bit7 -X248_bit8 -X248_bit9 -X248_bit10 -X248_bit11 -X248_bit12 -X249_bit_7 -X249_bit_6 -X249_bit_5 -X249_bit_4 -X249_bit_3 -X249_bit_2 -X249_bit_1 -X249_bit0 -X249_bit1 -X249_bit2 -X249_bit3 -X249_bit4 -X249_bit5 -X249_bit6 -X249_bit7 -X249_bit8 -X249_bit9 -X249_bit10 -X249_bit11 -X249_bit12 -X250_bit_7 -X250_bit_6 X250_bit_5 X250_bit_4 X250_bit_3 -X250_bit_2 -X250_bit_1 -X250_bit0 -X250_bit1 -X250_bit2 -X250_bit3 -X250_bit4 -X250_bit5 -X250_bit6 -X250_bit7 -X250_bit8 -X250_bit9 -X250_bit10 -X250_bit11 -X250_bit12 -X251_bit_7 -X251_bit_6 X251_bit_5 X251_bit_4 X251_bit_3 X251_bit_2 -X251_bit_1 X251_bit0 -X251_bit1 -X251_bit2 -X251_bit3 -X251_bit4 -X251_bit5 -X251_bit6 -X251_bit7 -X251_bit8 -X251_bit9 -X251_bit10 -X251_bit11 -X251_bit12 -X252_bit_7 X252_bit_6 X252_bit_5 -X252_bit_4 -X252_bit_3 -X252_bit_2 -X252_bit_1 -X252_bit0 -X252_bit1 -X252_bit2 -X252_bit3 -X252_bit4 -X252_bit5 -X252_bit6 -X252_bit7 -X252_bit8 -X252_bit9 -X252_bit10 -X252_bit11 -X252_bit12 -X253_bit_7 X253_bit_6 -X253_bit_5 -X253_bit_4 -X253_bit_3 -X253_bit_2 -X253_bit_1 -X253_bit0 -X253_bit1 -X253_bit2 -X253_bit3 -X253_bit4 -X253_bit5 -X253_bit6 -X253_bit7 -X253_bit8 -X253_bit9 -X253_bit10 -X253_bit11 -X253_bit12 X254_bit_7 X254_bit_6 X254_bit_5 -X254_bit_4 -X254_bit_3 X254_bit_2 -X254_bit_1 X254_bit0 -X254_bit1 -X254_bit2 -X254_bit3 -X254_bit4 -X254_bit5 -X254_bit6 -X254_bit7 -X254_bit8 -X254_bit9 -X254_bit10 -X254_bit11 -X254_bit12 -X255_bit_7 -X255_bit_6 -X255_bit_5 -X255_bit_4 -X255_bit_3 X255_bit_2 X255_bit_1 -X255_bit0 -X255_bit1 -X255_bit2 -X255_bit3 -X255_bit4 -X255_bit5 -X255_bit6 -X255_bit7 -X255_bit8 -X255_bit9 -X255_bit10 -X255_bit11 -X255_bit12 Y0_bit0 Y1_bit0 Y2_bit0 Y3_bit0 -Y4_bit0 Y5_bit0 -Y6_bit0 -Y7_bit0 Y8_bit0 -Y9_bit0 Y10_bit0 Y11_bit0 Y12_bit0 Y13_bit0 -Y14_bit0 Y15_bit0 Y16_bit0 Y17_bit0 -Y18_bit0 Y19_bit0 Y20_bit0 Y21_bit0 -Y22_bit0 -Y23_bit0 Y24_bit0 Y25_bit0 -Y26_bit0 -Y27_bit0 -Y28_bit0 Y29_bit0 -Y30_bit0 Y31_bit0 -Y32_bit0 Y33_bit0 Y34_bit0 -Y35_bit0 -Y36_bit0 Y37_bit0 Y38_bit0 -Y39_bit0 Y40_bit0 Y41_bit0 Y42_bit0 Y43_bit0 Y44_bit0 Y45_bit0 Y46_bit0 -Y47_bit0 Y48_bit0 Y49_bit0 Y50_bit0 -Y51_bit0 Y52_bit0 Y53_bit0 -Y54_bit0 Y55_bit0 Y56_bit0 -Y57_bit0 -Y58_bit0 -Y59_bit0 Y60_bit0 Y61_bit0 Y62_bit0 -Y63_bit0 Y64_bit0 -Y65_bit0 Y66_bit0 Y67_bit0 Y68_bit0 Y69_bit0 Y70_bit0 Y71_bit0 Y72_bit0 -Y73_bit0 Y74_bit0 Y75_bit0 Y76_bit0 Y77_bit0 Y78_bit0 Y79_bit0 -Y80_bit0 Y81_bit0 -Y82_bit0 -Y83_bit0 Y84_bit0 Y85_bit0 -Y86_bit0 -Y87_bit0 -Y88_bit0 Y89_bit0 Y90_bit0 Y91_bit0 Y92_bit0 Y93_bit0 Y94_bit0 -Y95_bit0 Y96_bit0 -Y97_bit0 Y98_bit0 Y99_bit0 Y100_bit0 Y101_bit0 -Y102_bit0 -Y103_bit0 Y104_bit0 Y105_bit0 Y106_bit0 Y107_bit0 -Y108_bit0 -Y109_bit0 -Y110_bit0 Y111_bit0 Y112_bit0 -Y113_bit0 Y114_bit0 Y115_bit0 Y116_bit0 Y117_bit0 -Y118_bit0 Y119_bit0 -Y120_bit0 -Y121_bit0 -Y122_bit0 Y123_bit0 -Y124_bit0 Y125_bit0 Y126_bit0 Y12#### 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.84 0.94 0.91 2/54 30443
Raw data (stat): 30443 (runsolver) R 30442 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544738529 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 1992 0 0 0 993 5 0 0 25 0 1 0 544738529 10723328 1959 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2618 1959 603 41 0 2577 0
vsize: 10472
[startup+20.0016 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 2091 0 0 0 1991 6 0 0 25 0 1 0 544738529 11177984 2058 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2729 2058 603 41 0 2688 0
vsize: 10916
[startup+30.0017 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 2247 0 0 0 2990 7 0 0 25 0 1 0 544738529 11886592 2214 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2902 2214 603 41 0 2861 0
vsize: 11608
[startup+40.0017 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 2791 0 0 0 3989 8 0 0 25 0 1 0 544738529 14168064 2758 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3459 2758 603 41 0 3418 0
vsize: 13836
[startup+50.0015 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 3485 0 0 0 4987 10 0 0 25 0 1 0 544738529 16994304 3452 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4149 3452 603 41 0 4108 0
vsize: 16596
[startup+60.002 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 3671 0 0 0 5987 10 0 0 25 0 1 0 544738529 17666048 3638 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4313 3638 603 41 0 4272 0
vsize: 17252
[startup+70.0021 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 3905 0 0 0 6986 11 0 0 25 0 1 0 544738529 18870272 3872 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4607 3872 603 41 0 4566 0
vsize: 18428
[startup+80.0019 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 4444 0 0 0 7984 13 0 0 25 0 1 0 544738529 21028864 4411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5134 4411 603 41 0 5093 0
vsize: 20536
[startup+90.0014 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 4705 0 0 0 8984 14 0 0 25 0 1 0 544738529 21975040 4672 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5365 4672 603 41 0 5324 0
vsize: 21460
[startup+100.005 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 5904 0 0 0 9980 17 0 0 25 0 1 0 544738529 26943488 5871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6578 5871 603 41 0 6537 0
vsize: 26312
[startup+110.014 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 6804 0 0 0 10979 19 0 0 25 0 1 0 544738529 30547968 6771 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7458 6771 603 41 0 7417 0
vsize: 29832
[startup+120.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7066 0 0 0 11979 20 0 0 25 0 1 0 544738529 31625216 7033 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7721 7033 603 41 0 7680 0
vsize: 30884
[startup+130.015 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 12978 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+140.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 13979 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+150.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 14979 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+160.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 15979 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+170.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 16980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+180.02 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 17980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+190.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 18980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223648 134555205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+200.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 19980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+210.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 20980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+220.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7325 0 0 0 21980 21 0 0 25 0 1 0 544738529 32702464 7292 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7984 7292 603 41 0 7943 0
vsize: 31936
[startup+230.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 7578 0 0 0 22980 22 0 0 25 0 1 0 544738529 33644544 7545 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8214 7545 603 41 0 8173 0
vsize: 32856
[startup+240.021 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14247 0 0 0 23965 37 0 0 25 0 1 0 544738529 56754176 12887 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12887 603 41 0 13815 0
vsize: 55424
[startup+250.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14250 0 0 0 24965 37 0 0 25 0 1 0 544738529 56754176 12890 4294967295 134512640 134672761 3221224544 3221223668 134566142 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12890 603 41 0 13815 0
vsize: 55424
[startup+260.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14252 0 0 0 25965 37 0 0 25 0 1 0 544738529 56754176 12892 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12892 603 41 0 13815 0
vsize: 55424
[startup+270.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14253 0 0 0 26965 37 0 0 25 0 1 0 544738529 56754176 12893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12893 603 41 0 13815 0
vsize: 55424
[startup+280.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14254 0 0 0 27965 37 0 0 25 0 1 0 544738529 56754176 12894 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12894 603 41 0 13815 0
vsize: 55424
[startup+290.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14254 0 0 0 28965 37 0 0 25 0 1 0 544738529 56754176 12894 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12894 603 41 0 13815 0
vsize: 55424
[startup+300.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14254 0 0 0 29965 37 0 0 25 0 1 0 544738529 56754176 12894 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12894 603 41 0 13815 0
vsize: 55424
[startup+310.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 30966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+320.023 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 31966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+330.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 32966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+340.022 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 33966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+350.023 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 34966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+360.024 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 35966 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+370.024 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 36967 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+380.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14255 0 0 0 37967 37 0 0 25 0 1 0 544738529 56754176 12895 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13856 12895 603 41 0 13815 0
vsize: 55424
[startup+390.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 38967 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+400.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 39967 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+410.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 40967 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+420.025 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 41967 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223600 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+430.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 42967 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+440.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 43968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+450.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 44968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+460.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 45968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+470.027 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 46968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+480.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 47968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+490.026 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 48968 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+500.027 s]
Raw data (loadavg): 1.08 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14358 0 0 0 49969 38 0 0 25 0 1 0 544738529 56893440 12956 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13890 12956 603 41 0 13849 0
vsize: 55560
[startup+510.028 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14586 0 0 0 50968 39 0 0 25 0 1 0 544738529 57839616 13184 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14121 13185 603 41 0 14080 0
vsize: 56484
[startup+520.028 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 14831 0 0 0 51967 40 0 0 25 0 1 0 544738529 58920960 13429 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14385 13429 603 41 0 14344 0
vsize: 57540
[startup+530.028 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 15572 0 0 0 52965 42 0 0 25 0 1 0 544738529 61874176 14170 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15106 14170 603 41 0 15065 0
vsize: 60424
[startup+540.028 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 15871 0 0 0 53963 43 0 0 25 0 1 0 544738529 63086592 14469 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15402 14469 603 41 0 15361 0
vsize: 61608
[startup+550.028 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 15955 0 0 0 54963 44 0 0 25 0 1 0 544738529 63488000 14553 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15500 14553 603 41 0 15459 0
vsize: 62000
[startup+560.029 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 16121 0 0 0 55963 44 0 0 25 0 1 0 544738529 64163840 14719 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15665 14719 603 41 0 15624 0
vsize: 62660
[startup+570.029 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 16224 0 0 0 56963 44 0 0 25 0 1 0 544738529 65089536 14822 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15891 14822 603 41 0 15850 0
vsize: 63564
[startup+580.028 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 16421 0 0 0 57962 45 0 0 25 0 1 0 544738529 65765376 15019 4294967295 134512640 134672761 3221224544 3221223640 1075347325 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16056 15019 603 41 0 16015 0
vsize: 64224
[startup+590.029 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 16591 0 0 0 58962 46 0 0 25 0 1 0 544738529 66437120 15189 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16220 15189 603 41 0 16179 0
vsize: 64880
[startup+600.029 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 16838 0 0 0 59961 47 0 0 25 0 1 0 544738529 67510272 15436 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16482 15436 603 41 0 16441 0
vsize: 65928
[startup+610.03 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 60960 47 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223844 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+620.03 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 61960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+630.03 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 62960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+640.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 63960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+650.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 64960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+660.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 65960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+670.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 66960 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+680.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 67961 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+690.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 68961 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+700.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 69961 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+710.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 70961 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+720.031 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 71961 48 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+730.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 72961 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+740.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 73961 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223648 134560013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+750.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 74961 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+760.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 75961 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+770.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 76962 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+780.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 77962 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17198 0 0 0 78962 49 0 0 25 0 1 0 544738529 68472832 15706 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15706 603 41 0 16676 0
vsize: 66868
[startup+800.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17430 0 0 0 79961 49 0 0 25 0 1 0 544738529 69550080 15938 4294967295 134512640 134672761 3221224544 3221223728 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16980 15938 603 41 0 16939 0
vsize: 67920
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 17944 0 0 0 80960 51 0 0 25 0 1 0 544738529 71581696 16452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17476 16452 603 41 0 17435 0
vsize: 69904
[startup+820.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 18246 0 0 0 81959 52 0 0 25 0 1 0 544738529 72822784 16754 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17779 16754 603 41 0 17738 0
vsize: 71116
[startup+830.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 18575 0 0 0 82959 53 0 0 25 0 1 0 544738529 74182656 17083 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18111 17083 603 41 0 18070 0
vsize: 72444
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 18965 0 0 0 83958 54 0 0 25 0 1 0 544738529 75800576 17473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18506 17473 603 41 0 18465 0
vsize: 74024
[startup+850.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 19238 0 0 0 84957 54 0 0 25 0 1 0 544738529 76881920 17746 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18770 17746 603 41 0 18729 0
vsize: 75080
[startup+860.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 19445 0 0 0 85957 55 0 0 25 0 1 0 544738529 77692928 17953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18968 17953 603 41 0 18927 0
vsize: 75872
[startup+870.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 19690 0 0 0 86956 56 0 0 25 0 1 0 544738529 78778368 18198 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19233 18198 603 41 0 19192 0
vsize: 76932
[startup+880.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 19873 0 0 0 87956 56 0 0 25 0 1 0 544738529 79462400 18381 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19400 18381 603 41 0 19359 0
vsize: 77600
[startup+890.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 20034 0 0 0 88956 57 0 0 25 0 1 0 544738529 80134144 18542 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19564 18542 603 41 0 19523 0
vsize: 78256
[startup+900.041 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 20241 0 0 0 89956 57 0 0 25 0 1 0 544738529 80945152 18749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19762 18749 603 41 0 19721 0
vsize: 79048
[startup+910.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 20611 0 0 0 90955 58 0 0 25 0 1 0 544738529 82432000 19119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20125 19119 603 41 0 20084 0
vsize: 80500
[startup+920.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 21016 0 0 0 91954 60 0 0 25 0 1 0 544738529 84045824 19524 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20519 19524 603 41 0 20478 0
vsize: 82076
[startup+930.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 21401 0 0 0 92953 61 0 0 25 0 1 0 544738529 85659648 19909 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20913 19909 603 41 0 20872 0
vsize: 83652
[startup+940.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 21693 0 0 0 93953 61 0 0 25 0 1 0 544738529 86876160 20201 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21210 20201 603 41 0 21169 0
vsize: 84840
[startup+950.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 21900 0 0 0 94952 62 0 0 25 0 1 0 544738529 87715840 20408 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21415 20408 603 41 0 21374 0
vsize: 85660
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 22067 0 0 0 95951 62 0 0 25 0 1 0 544738529 88387584 20575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21579 20575 603 41 0 21538 0
vsize: 86316
[startup+970.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 22283 0 0 0 96951 63 0 0 25 0 1 0 544738529 89194496 20791 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21776 20791 603 41 0 21735 0
vsize: 87104
[startup+980.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 22552 0 0 0 97950 64 0 0 25 0 1 0 544738529 90275840 21060 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22040 21060 603 41 0 21999 0
vsize: 88160
[startup+990.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 22817 0 0 0 98949 66 0 0 25 0 1 0 544738529 91369472 21325 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22307 21325 603 41 0 22266 0
vsize: 89228
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23074 0 0 0 99948 66 0 0 25 0 1 0 544738529 92442624 21582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22569 21582 603 41 0 22528 0
vsize: 90276
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23239 0 0 0 100948 66 0 0 25 0 1 0 544738529 93122560 21747 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21747 603 41 0 22694 0
vsize: 90940
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23240 0 0 0 101948 66 0 0 25 0 1 0 544738529 93122560 21748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21748 603 41 0 22694 0
vsize: 90940
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23240 0 0 0 102949 66 0 0 25 0 1 0 544738529 93122560 21748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21748 603 41 0 22694 0
vsize: 90940
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23241 0 0 0 103949 67 0 0 25 0 1 0 544738529 93122560 21749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21749 603 41 0 22694 0
vsize: 90940
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23246 0 0 0 104949 67 0 0 25 0 1 0 544738529 93122560 21754 4294967295 134512640 134672761 3221224544 3221223604 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21754 603 41 0 22694 0
vsize: 90940
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23246 0 0 0 105949 67 0 0 25 0 1 0 544738529 93122560 21754 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21754 603 41 0 22694 0
vsize: 90940
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23246 0 0 0 106949 67 0 0 25 0 1 0 544738529 93122560 21754 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21754 603 41 0 22694 0
vsize: 90940
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23248 0 0 0 107949 67 0 0 25 0 1 0 544738529 93122560 21756 4294967295 134512640 134672761 3221224544 3221223728 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21756 603 41 0 22694 0
vsize: 90940
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23248 0 0 0 108950 67 0 0 25 0 1 0 544738529 93122560 21756 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21756 603 41 0 22694 0
vsize: 90940
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23249 0 0 0 109950 67 0 0 25 0 1 0 544738529 93122560 21757 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21757 603 41 0 22694 0
vsize: 90940
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23249 0 0 0 110950 67 0 0 25 0 1 0 544738529 93122560 21757 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21757 603 41 0 22694 0
vsize: 90940
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23250 0 0 0 111950 67 0 0 25 0 1 0 544738529 93122560 21758 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21758 603 41 0 22694 0
vsize: 90940
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23258 0 0 0 112950 67 0 0 25 0 1 0 544738529 93122560 21766 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21766 603 41 0 22694 0
vsize: 90940
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23258 0 0 0 113950 67 0 0 25 0 1 0 544738529 93122560 21766 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22735 21766 603 41 0 22694 0
vsize: 90940
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23296 0 0 0 114950 67 0 0 25 0 1 0 544738529 93384704 21804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21804 603 41 0 22758 0
vsize: 91196
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23298 0 0 0 115950 67 0 0 25 0 1 0 544738529 93384704 21806 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21806 603 41 0 22758 0
vsize: 91196
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23299 0 0 0 116950 67 0 0 25 0 1 0 544738529 93384704 21807 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21807 603 41 0 22758 0
vsize: 91196
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23303 0 0 0 117950 67 0 0 25 0 1 0 544738529 93384704 21811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21811 603 41 0 22758 0
vsize: 91196
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23303 0 0 0 118950 67 0 0 25 0 1 0 544738529 93384704 21811 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21811 603 41 0 22758 0
vsize: 91196
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 30443
Raw data (stat): 30443 (minisat+) R 30442 27222 27221 0 -1 0 23303 0 0 0 119950 67 0 0 25 0 1 0 544738529 93384704 21811 4294967295 134512640 134672761 3221224544 3221223668 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22799 21811 603 41 0 22758 0
vsize: 91196
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 30443
Raw data (stat): 30443 (minisat+) Z 30442 27222 27221 0 -1 12 23306 0 0 0 119951 71 0 0 25 0 1 0 544738529 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.24
CPU user time (s): 1199.52
CPU system time (s): 0.71789
CPU usage (%): 100.011
Max. virtual memory (Kb): 91196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####