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/MIPLIB/miplib2003/normalized-mps-v2-13-7-rout.opb
MD5SUM	46c175563919d1fe493ed3da6f49d52f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1251872
Optimality of the best value was proved	NO
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	33812000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	166074535
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1585.77
Number of variables	5151
Total number of constraints	606
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	314
Number of constraints which are nor clauses,nor cardinality constraints	292
Minimum length of a constraint	1
Maximum length of a constraint	617
Trace number 18465

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-21 15:08:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17984 boxname=wulflinc10 idbench=1384 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  46c175563919d1fe493ed3da6f49d52f  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-rout.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-rout.opb
IDLAUNCH: 17984
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        788256 kB
Buffers:         11904 kB
Cached:         212836 kB
SwapCached:          0 kB
Active:          25724 kB
Inactive:       201524 kB
HighTotal:      131008 kB
HighFree:        33236 kB
LowTotal:       903652 kB
LowFree:        755020 kB
SwapTotal:     2097136 kB
SwapFree:      2096784 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6412 kB
Slab:            13648 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:28:05 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 17984 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 337 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################
c   -- Clauses(.)/Splits(s): ...............
c ---[ 320]---> Adder-cost: 3854   maxlim: 97129415   bits: 27/27
c ---[ 319]---> BDD-cost:   37
c ---[ 318]---> BDD-cost:   13
c ---[ 317]---> BDD-cost:   13
c ---[ 316]---> BDD-cost:   25
c ---[ 315]---> BDD-cost:   25
c ---[ 314]---> BDD-cost:   25
c ---[ 313]---> BDD-cost:   25
c ---[ 312]---> BDD-cost:   25
c ---[ 311]---> BDD-cost:   25
c ---[ 310]---> BDD-cost:   25
c ---[ 309]---> BDD-cost:   25
c ---[ 308]---> BDD-cost:   37
c ---[ 307]---> BDD-cost:   25
c ---[ 306]---> BDD-cost:   25
c ---[ 305]---> BDD-cost:   13
c ---[ 304]---> BDD-cost:   13
c ---[ 303]---> BDD-cost:   13
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 299]---> BDD-cost:   13
c ---[ 298]---> BDD-cost:   13
c ---[ 297]---> BDD-cost:   37
c ---[ 296]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 293]---> BDD-cost:   13
c ---[ 292]---> BDD-cost:   13
c ---[ 291]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   13
c ---[ 289]---> BDD-cost:   13
c ---[ 288]---> BDD-cost:   13
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   37
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 281]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 275]---> BDD-cost:   37
c ---[ 274]---> BDD-cost:   13
c ---[ 273]---> BDD-cost:   13
c ---[ 272]---> BDD-cost:   13
c ---[ 271]---> BDD-cost:   13
c ---[ 270]---> BDD-cost:   13
c ---[ 269]---> BDD-cost:   13
c ---[ 268]---> BDD-cost:   13
c ---[ 267]---> BDD-cost:   13
c ---[ 266]---> BDD-cost:   13
c ---[ 265]---> BDD-cost:   13
c ---[ 264]---> BDD-cost:   37
c ---[ 263]---> BDD-cost:   13
c ---[ 262]---> BDD-cost:   13
c ---[ 261]---> BDD-cost:   13
c ---[ 260]---> BDD-cost:   13
c ---[ 259]---> BDD-cost:   13
c ---[ 258]---> BDD-cost:   13
c ---[ 257]---> BDD-cost:   13
c ---[ 256]---> BDD-cost:   13
c ---[ 255]---> BDD-cost:   13
c ---[ 254]---> BDD-cost:   13
c ---[ 253]---> BDD-cost:   37
c ---[ 252]---> BDD-cost:   13
c ---[ 251]---> BDD-cost:   13
c ---[ 250]---> BDD-cost:   13
c ---[ 249]---> BDD-cost:   13
c ---[ 248]---> BDD-cost:   13
c ---[ 247]---> BDD-cost:   13
c ---[ 246]---> BDD-cost:   13
c ---[ 245]---> BDD-cost:   13
c ---[ 244]---> BDD-cost:   13
c ---[ 243]---> BDD-cost:   13
c ---[ 242]---> BDD-cost:   37
c ---[ 241]---> BDD-cost:   13
c ---[ 240]---> BDD-cost:   13
c ---[ 239]---> BDD-cost:   13
c ---[ 238]---> BDD-cost:   13
c ---[ 237]---> BDD-cost:   13
c ---[ 236]---> BDD-cost:   13
c ---[ 235]---> BDD-cost:   13
c ---[ 234]---> BDD-cost:   13
c ---[ 233]---> BDD-cost:   13
c ---[ 232]---> BDD-cost:   13
c ---[ 231]---> BDD-cost:   37
c ---[ 230]---> BDD-cost:   13
c ---[ 229]---> BDD-cost:   13
c ---[ 228]---> BDD-cost:   13
c ---[ 227]---> BDD-cost:   13
c ---[ 226]---> BDD-cost:   13
c ---[ 225]---> BDD-cost:   13
c ---[ 224]---> BDD-cost:   13
c ---[ 223]---> BDD-cost:   13
c ---[ 222]---> BDD-cost:   13
c ---[ 221]---> BDD-cost:   13
c ---[ 220]---> BDD-cost:   37
c ---[ 219]---> BDD-cost:   13
c ---[ 218]---> BDD-cost:   13
c ---[ 217]---> BDD-cost:   13
c ---[ 216]---> BDD-cost:   13
c ---[ 215]---> BDD-cost:   13
c ---[ 214]---> BDD-cost:   13
c ---[ 213]---> BDD-cost:   13
c ---[ 212]---> BDD-cost:   13
c ---[ 211]---> BDD-cost:   13
c ---[ 210]---> BDD-cost:   13
c ---[ 209]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[ 208]---> BDD-cost:   37
c ---[ 207]---> BDD-cost:   13
c ---[ 206]---> BDD-cost:   13
c ---[ 205]---> BDD-cost:   13
c ---[ 204]---> BDD-cost:   13
c ---[ 203]---> BDD-cost:   13
c ---[ 202]---> BDD-cost:   13
c ---[ 201]---> BDD-cost:   13
c ---[ 200]---> BDD-cost:   13
c ---[ 199]---> BDD-cost:   13
c ---[ 198]---> BDD-cost:   13
c ---[ 197]---> BDD-cost:   37
c ---[ 196]---> BDD-cost:   13
c ---[ 195]---> BDD-cost:   13
c ---[ 194]---> BDD-cost:   13
c ---[ 193]---> BDD-cost:   13
c ---[ 192]---> BDD-cost:   13
c ---[ 191]---> BDD-cost:   13
c ---[ 190]---> BDD-cost:   13
c ---[ 189]---> BDD-cost:   13
c ---[ 188]---> BDD-cost:   13
c ---[ 187]---> BDD-cost:   13
c ---[ 185]---> Sorter-cost:  441     Base: 2
c ---[ 184]---> BDD-cost:   13
c ---[ 183]---> BDD-cost:   13
c ---[ 182]---> BDD-cost:   13
c ---[ 181]---> BDD-cost:   13
c ---[ 180]---> BDD-cost:   13
c ---[ 179]---> BDD-cost:   13
c ---[ 178]---> BDD-cost:   13
c ---[ 177]---> BDD-cost:   13
c ---[ 176]---> BDD-cost:   13
c ---[ 175]---> BDD-cost:   13
c ---[ 173]---> Sorter-cost:  441     Base: 2
c ---[ 172]---> BDD-cost:   13
c ---[ 171]---> BDD-cost:   13
c ---[ 170]---> BDD-cost:   13
c ---[ 169]---> BDD-cost:   13
c ---[ 168]---> BDD-cost:   13
c ---[ 167]---> BDD-cost:   13
c ---[ 166]---> BDD-cost:   13
c ---[ 165]---> BDD-cost:   13
c ---[ 164]---> BDD-cost:   13
c ---[ 163]---> BDD-cost:   13
c ---[ 161]---> Sorter-cost:  441     Base: 2
c ---[ 160]---> BDD-cost:   13
c ---[ 159]---> BDD-cost:   13
c ---[ 158]---> BDD-cost:   13
c ---[ 157]---> BDD-cost:   13
c ---[ 156]---> BDD-cost:   13
c ---[ 155]---> BDD-cost:   13
c ---[ 154]---> BDD-cost:   13
c ---[ 153]---> BDD-cost:   13
c ---[ 152]---> BDD-cost:   13
c ---[ 151]---> BDD-cost:   13
c ---[ 149]---> Sorter-cost:  441     Base: 2
c ---[ 148]---> BDD-cost:   13
c ---[ 147]---> BDD-cost:   13
c ---[ 146]---> BDD-cost:   13
c ---[ 145]---> BDD-cost:   13
c ---[ 144]---> BDD-cost:   13
c ---[ 143]---> BDD-cost:   13
c ---[ 142]---> BDD-cost:   13
c ---[ 141]---> BDD-cost:   13
c ---[ 140]---> BDD-cost:   13
c ---[ 139]---> BDD-cost:   13
c ---[ 137]---> Sorter-cost:  441     Base: 2
c ---[ 136]---> BDD-cost:   13
c ---[ 135]---> BDD-cost:   13
c ---[ 134]---> BDD-cost:   13
c ---[ 133]---> BDD-cost:   13
c ---[ 132]---> BDD-cost:   13
c ---[ 131]---> BDD-cost:   13
c ---[ 130]---> BDD-cost:   13
c ---[ 129]---> BDD-cost:   13
c ---[ 128]---> BDD-cost:   13
c ---[ 127]---> BDD-cost:   13
c ---[ 125]---> Sorter-cost:  347     Base: 2
c ---[ 124]---> BDD-cost:   13
c ---[ 123]---> BDD-cost:   13
c ---[ 122]---> BDD-cost:   13
c ---[ 121]---> BDD-cost:   13
c ---[ 120]---> BDD-cost:   13
c ---[ 119]---> BDD-cost:   13
c ---[ 118]---> BDD-cost:   13
c ---[ 117]---> BDD-cost:   13
c ---[ 116]---> BDD-cost:   13
c ---[ 115]---> BDD-cost:   13
c ---[ 113]---> Sorter-cost:  347     Base: 2
c ---[ 112]---> BDD-cost:   13
c ---[ 111]---> BDD-cost:   13
c ---[ 110]---> BDD-cost:   13
c ---[ 109]---> BDD-cost:   13
c ---[ 108]---> BDD-cost:   13
c ---[ 107]---> BDD-cost:   13
c ---[ 106]---> BDD-cost:   13
c ---[ 105]---> BDD-cost:   13
c ---[ 104]---> BDD-cost:   13
c ---[ 103]---> BDD-cost:   13
c ---[ 101]---> Sorter-cost:  347     Base: 2
c ---[ 100]---> BDD-cost:   13
c ---[  99]---> BDD-cost:   13
c ---[  98]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  96]---> Sorter-cost:  347     Base: 2
c ---[  94]---> Sorter-cost:  347     Base: 2
c ---[  92]---> Sorter-cost:  515     Base: 2
c ---[  90]---> Sorter-cost:  515     Base: 2
c ---[  88]---> Sorter-cost:  515     Base: 2
c ---[  86]---> Sorter-cost:  515     Base: 2
c ---[  84]---> Sorter-cost:  515     Base: 2
c ---[  82]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  80]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  78]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  77]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  75]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  73]---> Adder-cost: 548   maxlim: 21489   bits: 16/15
c ---[  71]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  69]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  67]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  65]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  63]---> Adder-cost: 460   maxlim: 9207   bits: 15/14
c ---[  61]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  59]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  57]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  56]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  54]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  52]---> Adder-cost: 624   maxlim: 21483   bits: 16/15
c ---[  51]---> BDD-cost:   13
c ---[  50]---> BDD-cost:   13
c ---[  49]---> BDD-cost:   13
c ---[  48]---> BDD-cost:   13
c ---[  47]---> BDD-cost:   13
c ---[  46]---> BDD-cost:   13
c ---[  45]---> BDD-cost:   13
c ---[  44]---> BDD-cost:   13
c ---[  43]---> Adder-cost: 604   maxlim: 25598   bits: 15/15
c ---[  42]---> BDD-cost:   13
c ---[  41]---> BDD-cost:   13
c ---[  40]---> BDD-cost:   13
c ---[  39]---> BDD-cost:   13
c ---[  38]---> BDD-cost:   13
c ---[  37]---> BDD-cost:   13
c ---[  36]---> BDD-cost:   13
c ---[  35]---> BDD-cost:   13
c ---[  34]---> BDD-cost:   13
c ---[  33]---> BDD-cost:   13
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   13
c ---[  30]---> BDD-cost:   13
c ---[  29]---> BDD-cost:   13
c ---[  28]---> BDD-cost:   13
c ---[  27]---> BDD-cost:   13
c ---[  26]---> BDD-cost:   13
c ---[  25]---> BDD-cost:   13
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   13
c ---[  22]---> BDD-cost:   13
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   13
c ---[  19]---> BDD-cost:   13
c ---[  18]---> BDD-cost:   13
c ---[  17]---> BDD-cost:   13
c ---[  16]---> BDD-cost:   13
c ---[  15]---> BDD-cost:   13
c ---[  14]---> BDD-cost:   13
c ---[  13]---> BDD-cost:   13
c ---[  12]---> BDD-cost:   13
c ---[  11]---> BDD-cost:   13
c ---[  10]---> BDD-cost:   84
c ---[   9]---> BDD-cost:   13
c ---[   8]---> BDD-cost:   13
c ---[   7]---> BDD-cost:   13
c ---[   6]---> BDD-cost:   13
c ---[   5]---> BDD-cost:   13
c ---[   4]---> BDD-cost:   13
c ---[   3]---> BDD-cost:   13
c ---[   2]---> BDD-cost:   13
c ---[   1]---> BDD-cost:   13
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  124804   419096 |   41601       0        0     nan |  0.000 % |
c |       100 |  124787   419037 |   45761      99      720     7.3 | 12.396 % |
c |       250 |  124746   418945 |   50337     248     7490    30.2 | 12.432 % |
c |       475 |  124714   418841 |   55370     468    17116    36.6 | 12.454 % |
c |       813 |  124714   418841 |   60908     806    33196    41.2 | 12.454 % |
c |      1319 |  124714   418841 |   66998    1312    52363    39.9 | 12.454 % |
c |      2078 |  124701   418803 |   73698    2069    86927    42.0 | 12.464 % |
c |      3217 |  124701   418803 |   81068    3208   147143    45.9 | 12.464 % |
c |      4925 |  123998   417190 |   89175    4867   217171    44.6 | 13.214 % |
c |      7487 |  123721   416507 |   98092    7373   318542    43.2 | 13.491 % |
c |     11331 |  123452   415827 |  107902   11200   516430    46.1 | 13.736 % |
c |     17099 |  123047   414830 |  118692   16935   792369    46.8 | 14.125 % |
c |     25748 |  122597   413692 |  130561   25527  1102299    43.2 | 14.560 % |
c |     38726 |  121236   410347 |  143617   38328  1804764    47.1 | 15.915 % |
c |     58187 |  120625   408822 |  157979   57700  2730186    47.3 | 16.527 % |
c |     87379 |  119228   405216 |  173777   86682  5043575    58.2 | 17.816 % |
c ==============================================================================
c [1mFound solution: 1274336[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89427 |  119132   404986 |   39710   88726  5141418    57.9 | 17.816 % |
c |     89529 |  119062   404794 |   43681   20530   973122    47.4 | 18.010 % |
c |     89679 |  119062   404794 |   48049   20680   981513    47.5 | 18.010 % |
c |     89906 |  119062   404794 |   52854   20907   992789    47.5 | 18.010 % |
c |     90246 |  119000   404650 |   58139   21245  1012788    47.7 | 18.085 % |
c |     90752 |  118991   404619 |   63953   21747  1036653    47.7 | 18.089 % |
c |     91512 |  118966   404563 |   70348   22505  1063487    47.3 | 18.114 % |
c |     92651 |  118958   404537 |   77383   23643  1112361    47.0 | 18.118 % |
c |     94359 |  118878   404308 |   85121   25338  1216426    48.0 | 18.186 % |
c |     96922 |  118651   403664 |   93634   27883  1650025    59.2 | 18.373 % |
c ==============================================================================
c [1mFound solution: 1270944[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98762 |  118669   403707 |   39556   29723  1793169    60.3 | 18.373 % |
c |     98864 |  118669   403707 |   43511   29825  1795039    60.2 | 18.370 % |
c |     99015 |  118669   403707 |   47862   29976  1797707    60.0 | 18.370 % |
c |     99242 |  118669   403707 |   52649   30203  1802568    59.7 | 18.370 % |
c |     99579 |  118661   403681 |   57913   30538  1814512    59.4 | 18.385 % |
c |    100087 |  118613   403571 |   63705   31044  1835975    59.1 | 18.428 % |
c |    100846 |  118507   403284 |   70075   31787  1899914    59.8 | 18.518 % |
c |    101986 |  118462   403182 |   77083   32924  2022256    61.4 | 18.568 % |
c |    103696 |  118454   403156 |   84791   34633  2187604    63.2 | 18.572 % |
c |    106259 |  118365   402943 |   93270   37187  2412028    64.9 | 18.673 % |
c |    110104 |  118155   402321 |  102598   41003  2861607    69.8 | 18.838 % |
c |    115871 |  118097   402180 |  112857   46766  3298451    70.5 | 18.907 % |
c |    124520 |  118075   402109 |  124143   55408  3779430    68.2 | 18.917 % |
c |    137494 |  117617   400754 |  136558   68271  4724688    69.2 | 19.227 % |
c |    156958 |  116259   396059 |  150213   87491  5933242    67.8 | 19.716 % |
c ==============================================================================
c [1mFound solution: 1235840[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    185993 |  115137   392341 |   38379  116225  8922288    76.8 | 19.716 % |
c |    186094 |  115137   392341 |   42216   27083  1286243    47.5 | 20.314 % |
c |    186244 |  115137   392341 |   46438   27233  1294486    47.5 | 20.314 % |
c |    186469 |  115137   392341 |   51082   27458  1316364    47.9 | 20.314 % |
c |    186807 |  115137   392341 |   56190   27796  1321287    47.5 | 20.314 % |
c |    187313 |  115003   391979 |   61809   28282  1349492    47.7 | 20.458 % |
c |    188072 |  115003   391979 |   67990   29041  1384593    47.7 | 20.458 % |
c |    189214 |  115003   391979 |   74789   30183  1429382    47.4 | 20.458 % |
c |    190922 |  114925   391736 |   82268   31885  1681516    52.7 | 20.505 % |
c |    193485 |  114870   391545 |   90495   34437  1873869    54.4 | 20.534 % |
c |    197332 |  114858   391510 |   99545   38280  2133369    55.7 | 20.541 % |
c |    203098 |  114850   391492 |  109499   44041  3215607    73.0 | 20.548 % |
c |    211747 |  114653   390887 |  120449   52648  4076407    77.4 | 20.678 % |
c |    224722 |  114617   390797 |  132494   65615  4763741    72.6 | 20.714 % |
c |    244184 |  114562   390672 |  145744   85073  7752740    91.1 | 20.779 % |
c |    273376 |  114170   389482 |  160318  114178 12301535   107.7 | 21.084 % |
c |    317166 |  113847   388410 |  176350  157899 19720184   124.9 | 21.282 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 x241_bit13 x242_bit0 -x243_bit0 x244_bit0 x245_bit0 x246_bit0 -x247_bit0 x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 x252_bit0 -x253_bit0 x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 -x259_bit0 -x260_bit0 -x261_bit0 -x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 -x267_bit0 -x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 -x275_bit0 -x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 -x287_bit0 -x288_bit0 -x289_bit0 -x290_bit0 -x291_bit0 -x292_bit0 -x293_bit0 -x294_bit0 -x295_bit0 -x296_bit0 -x297_bit0 -x298_bit0 -x299_bit0 -x300_bit0 -x301_bit0 -x302_bit0 -x302_bit1 -x303_bit0 -x303_bit1 -x304_bit0 -x304_bit1 -x305_bit0 -x305_bit1 -x306_bit0 -x306_bit1 -x307_bit0 -x307_bit1 -x308_bit0 -x308_bit1 -x309_bit0 -x309_bit1 -x310_bit0 -x310_bit1 -x311_bit0 -x311_bit1 -x312_bit0 -x312_bit1 -x313_bit0 -x313_bit1 -x314_bit0 -x314_bit1 x315_bit0 -x315_bit1 x316_bit0 -x316_bit1 -x317_bit0 x318_bit0 -x319_bit0 -x320_bit0 -x321_bit0 -x322_bit0 -x323_bit0 -x324_bit0 -x325_bit0 -x326_bit0 -x327_bit0 -x328_bit0 -x329_bit0 -x330_bit0 -x331_bit0 -x332_bit0 -x333_bit0 -x334_bit0 -x335_bit0 -x336_bit0 -x337_bit0 -x338_bit0 -x339_bit0 -x340_bit0 -x341_bit0 -x342_bit0 -x343_bit0 -x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 -x351_bit0 -x352_bit0 -x353_bit0 x354_bit0 -x355_bit0 -x356_bit0 x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 -x373_bit0 -x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 -x379_bit0 -x380_bit0 -x381_bit0 -x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 -x390_bit0 -x391_bit0 -x392_bit0 x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 x400_bit0 -x401_bit0 -x402_bit0 -x403_bit0 -x404_bit0 -x405_bit0 -x406_bit0 -x407_bit0 -x408_bit0 -x409_bit0 -x410_bit0 -x411_bit0 -x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 -x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 -x423_bit0 -x424_bit0 -x425_bit0 -x426_bit0 -x427_bit0 -x428_bit0 -x429_bit0 -x430_bit0 -x431_bit0 -x432_bit0 -x433_bit0 -x434_bit0 -x435_bit0 -x436_bit0 -x437_bit0 -x438_bit0 x439_bit0 -x440_bit0 -x441_bit0 -x442_bit0 -x443_bit0 -x444_bit0 -x445_bit0 -x446_bit0 -x447_bit0 -x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 -x452_bit0 -x453_bit0 -x454_bit0 -x455_bit0 -x456_bit0 x457_bit0 -x458_bit0 -x459_bit0 -x460_bit0 -x461_bit0 -x462_bit0 -x463_bit0 -x464_bit0 -x465_bit0 -x466_bit0 -x467_bit0 -x468_bit0 -x469_bit0 -x470_bit0 -x471_bit0 -x472_bit0 -x473_bit0 -x474_bit0 -x475_bit0 -x476_bit0 -x477_bit0 -x478_bit0 -x479_bit0 -x480_bit0 -x481_bit0 -x482_bit0 -x483_bit0 -x484_bit0 -x485_bit0 -x486_bit0 -x487_bit0 -x488_bit0 -x489_bit0 x490_bit0 -x491_bit0 -x492_bit0 -x493_bit0 -x494_bit0 -x495_bit0 -x496_bit0 -x497_bit0 -x498_bit0 x499_bit0 -x500_bit0 -x501_bit0 -x502_bit0 -x503_bit0 -x504_bit0 -x505_bit0 -x506_bit0 -x507_bit0 -x508_bit0 -x509_bit0 -x510_bit0 -x511_bit0 -x512_bit0 -x513_bit0 -x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 -x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 x524_bit0 -x525_bit0 -x526_bit0 -x527_bit0 -x528_bit0 -x529_bit0 -x530_bit0 -x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 -x538_bit0 -x539_bit0 -x540_bit0 x541_bit0 -x542_bit0 -x543_bit0 -x544_bit0 -x545_bit0 -x546_bit0 -x547_bit0 -x548_bit0 -x549_bit0 -x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 -x554_bit0 -x555_bit0 -x556_bit0 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -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 -#### 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.79 0.94 0.92 2/54 1259
Raw data (stat): 1259 (runsolver) R 1258 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487825525 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0001 s]
Raw data (loadavg): 0.83 0.94 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 1062 0 0 0 995 3 0 0 25 0 1 0 487825525 4886528 749 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1193 749 603 41 0 1152 0
vsize: 4772
[startup+20.0005 s]
Raw data (loadavg): 0.85 0.94 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 3739 0 0 0 1988 9 0 0 25 0 1 0 487825525 15417344 3291 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3764 3291 603 41 0 3723 0
vsize: 15056
[startup+30.0014 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 3895 0 0 0 2987 10 0 0 25 0 1 0 487825525 16084992 3447 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3927 3447 603 41 0 3886 0
vsize: 15708
[startup+40.0022 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 4060 0 0 0 3986 11 0 0 25 0 1 0 487825525 16748544 3612 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4089 3612 603 41 0 4048 0
vsize: 16356
[startup+50.0021 s]
Raw data (loadavg): 0.91 0.94 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 4281 0 0 0 4985 12 0 0 25 0 1 0 487825525 17678336 3833 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4316 3833 603 41 0 4275 0
vsize: 17264
[startup+60.0019 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 4511 0 0 0 5984 12 0 0 25 0 1 0 487825525 18624512 4063 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4547 4063 603 41 0 4506 0
vsize: 18188
[startup+70.0025 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 4810 0 0 0 6983 14 0 0 25 0 1 0 487825525 19869696 4362 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4851 4362 603 41 0 4810 0
vsize: 19404
[startup+80.0029 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 5124 0 0 0 7982 15 0 0 25 0 1 0 487825525 21065728 4676 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5143 4676 603 41 0 5102 0
vsize: 20572
[startup+90.0028 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 5440 0 0 0 8981 16 0 0 25 0 1 0 487825525 22413312 4992 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5472 4992 603 41 0 5431 0
vsize: 21888
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 5671 0 0 0 9979 17 0 0 25 0 1 0 487825525 23478272 5223 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5732 5223 603 41 0 5691 0
vsize: 22928
[startup+110.004 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 5901 0 0 0 10978 18 0 0 25 0 1 0 487825525 24412160 5453 4294967295 134512640 134672761 3221224624 3221223776 134565101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5960 5453 603 41 0 5919 0
vsize: 23840
[startup+120.008 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 6059 0 0 0 11977 19 0 0 25 0 1 0 487825525 25083904 5611 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6124 5611 603 41 0 6083 0
vsize: 24496
[startup+130.015 s]
Raw data (loadavg): 1.05 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 6464 0 0 0 12977 20 0 0 25 0 1 0 487825525 26689536 6016 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6516 6016 603 41 0 6475 0
vsize: 26064
[startup+140.014 s]
Raw data (loadavg): 1.04 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 6730 0 0 0 13975 22 0 0 25 0 1 0 487825525 27758592 6282 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6777 6282 603 41 0 6736 0
vsize: 27108
[startup+150.016 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 7004 0 0 0 14974 23 0 0 25 0 1 0 487825525 28823552 6556 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7037 6556 603 41 0 6996 0
vsize: 28148
[startup+160.032 s]
Raw data (loadavg): 1.03 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 7370 0 0 0 15975 24 0 0 25 0 1 0 487825525 30289920 6922 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7395 6922 603 41 0 7354 0
vsize: 29580
[startup+170.033 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 7763 0 0 0 16973 26 0 0 25 0 1 0 487825525 32157696 7315 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7851 7315 603 41 0 7810 0
vsize: 31404
[startup+180.038 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 7930 0 0 0 17973 26 0 0 25 0 1 0 487825525 32837632 7482 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8017 7482 603 41 0 7976 0
vsize: 32068
[startup+190.055 s]
Raw data (loadavg): 1.02 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 8549 0 0 0 18973 28 0 0 25 0 1 0 487825525 35385344 8101 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8639 8101 603 41 0 8598 0
vsize: 34556
[startup+200.06 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 8726 0 0 0 19973 29 0 0 25 0 1 0 487825525 36052992 8278 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8802 8278 603 41 0 8761 0
vsize: 35208
[startup+210.059 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9038 0 0 0 20972 30 0 0 25 0 1 0 487825525 37384192 8590 4294967295 134512640 134672761 3221224624 3221223728 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9127 8590 603 41 0 9086 0
vsize: 36508
[startup+220.067 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9316 0 0 0 21971 31 0 0 25 0 1 0 487825525 38457344 8868 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9389 8868 603 41 0 9348 0
vsize: 37556
[startup+230.086 s]
Raw data (loadavg): 1.01 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9577 0 0 0 22973 32 0 0 25 0 1 0 487825525 39530496 9129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9651 9129 603 41 0 9610 0
vsize: 38604
[startup+240.086 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9718 0 0 0 23971 33 0 0 25 0 1 0 487825525 40148992 9270 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9802 9270 603 41 0 9761 0
vsize: 39208
[startup+250.09 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9718 0 0 0 24972 33 0 0 25 0 1 0 487825525 40148992 9270 4294967295 134512640 134672761 3221224624 3221223760 134565143 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9802 9270 603 41 0 9761 0
vsize: 39208
[startup+260.099 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 25972 33 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+270.1 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 26972 33 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223808 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+280.104 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 27972 34 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+290.104 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 28972 34 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+300.104 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 29972 34 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+310.106 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 30972 34 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+320.115 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 31972 35 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223796 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+330.122 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 32972 35 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223728 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+340.133 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 33973 35 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+350.134 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9746 0 0 0 34973 35 0 0 25 0 1 0 487825525 40374272 9298 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9298 603 41 0 9816 0
vsize: 39428
[startup+360.138 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 9770 0 0 0 35973 36 0 0 25 0 1 0 487825525 40374272 9322 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9857 9322 603 41 0 9816 0
vsize: 39428
[startup+370.148 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 10091 0 0 0 36973 37 0 0 25 0 1 0 487825525 41705472 9643 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10182 9643 603 41 0 10141 0
vsize: 40728
[startup+380.163 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 10297 0 0 0 37974 37 0 0 25 0 1 0 487825525 42508288 9849 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10378 9849 603 41 0 10337 0
vsize: 41512
[startup+390.163 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 10552 0 0 0 38973 38 0 0 25 0 1 0 487825525 43556864 10104 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10634 10104 603 41 0 10593 0
vsize: 42536
[startup+400.163 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 10745 0 0 0 39972 39 0 0 25 0 1 0 487825525 44363776 10297 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10831 10297 603 41 0 10790 0
vsize: 43324
[startup+410.163 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 10950 0 0 0 40972 40 0 0 25 0 1 0 487825525 45301760 10502 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11060 10502 603 41 0 11019 0
vsize: 44240
[startup+420.163 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 11610 0 0 0 41970 42 0 0 25 0 1 0 487825525 47951872 11162 4294967295 134512640 134672761 3221224624 3221223808 134559532 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11707 11162 603 41 0 11666 0
vsize: 46828
[startup+430.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 12009 0 0 0 42969 43 0 0 25 0 1 0 487825525 49557504 11561 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12099 11561 603 41 0 12058 0
vsize: 48396
[startup+440.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 12541 0 0 0 43967 45 0 0 25 0 1 0 487825525 51695616 12093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12621 12093 603 41 0 12580 0
vsize: 50484
[startup+450.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 12783 0 0 0 44966 46 0 0 25 0 1 0 487825525 52629504 12335 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12849 12335 603 41 0 12808 0
vsize: 51396
[startup+460.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13130 0 0 0 45965 47 0 0 25 0 1 0 487825525 54083584 12682 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13204 12682 603 41 0 13163 0
vsize: 52816
[startup+470.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13466 0 0 0 46964 49 0 0 25 0 1 0 487825525 55406592 13018 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13527 13018 603 41 0 13486 0
vsize: 54108
[startup+480.165 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13468 0 0 0 47964 49 0 0 25 0 1 0 487825525 55537664 13020 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13559 13020 603 41 0 13518 0
vsize: 54236
[startup+490.164 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13585 0 0 0 48963 50 0 0 25 0 1 0 487825525 55943168 13137 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13658 13137 603 41 0 13617 0
vsize: 54632
[startup+500.165 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13747 0 0 0 49963 50 0 0 25 0 1 0 487825525 56606720 13299 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13820 13299 603 41 0 13779 0
vsize: 55280
[startup+510.165 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 50962 51 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+520.165 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 51962 51 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+530.166 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 52962 51 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+540.166 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 53962 51 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+550.166 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 54962 52 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+560.166 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 55961 52 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+570.167 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 56961 52 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+580.168 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 57961 53 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+590.167 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 58961 53 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223760 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+600.168 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 59960 53 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+610.168 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 60960 54 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+620.169 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 61960 54 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+630.169 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 62960 54 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+640.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 63960 55 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+650.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 64960 55 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+660.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 65960 55 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223728 134560474 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+670.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 66960 55 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+680.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 67960 55 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+690.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 68959 56 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+700.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 13954 0 0 0 69959 56 0 0 25 0 1 0 487825525 57413632 13506 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 13506 603 41 0 13976 0
vsize: 56068
[startup+710.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 14666 0 0 0 70958 58 0 0 25 0 1 0 487825525 60334080 14218 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14730 14218 603 41 0 14689 0
vsize: 58920
[startup+720.17 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 14854 0 0 0 71957 58 0 0 25 0 1 0 487825525 61145088 14406 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14928 14406 603 41 0 14887 0
vsize: 59712
[startup+730.171 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 15115 0 0 0 72956 59 0 0 25 0 1 0 487825525 62214144 14667 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15189 14667 603 41 0 15148 0
vsize: 60756
[startup+740.171 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 15449 0 0 0 73955 60 0 0 25 0 1 0 487825525 63553536 15001 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15516 15001 603 41 0 15475 0
vsize: 62064
[startup+750.171 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 15952 0 0 0 74954 62 0 0 25 0 1 0 487825525 65683456 15504 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16036 15504 603 41 0 15995 0
vsize: 64144
[startup+760.172 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 16345 0 0 0 75953 63 0 0 25 0 1 0 487825525 67293184 15897 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16429 15897 603 41 0 16388 0
vsize: 65716
[startup+770.172 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 16865 0 0 0 76952 64 0 0 25 0 1 0 487825525 69427200 16417 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 16417 603 41 0 16909 0
vsize: 67800
[startup+780.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 17317 0 0 0 77951 65 0 0 25 0 1 0 487825525 71159808 16869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17373 16869 603 41 0 17332 0
vsize: 69492
[startup+790.172 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 17666 0 0 0 78950 66 0 0 25 0 1 0 487825525 72634368 17218 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17733 17218 603 41 0 17692 0
vsize: 70932
[startup+800.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 18000 0 0 0 79949 67 0 0 25 0 1 0 487825525 73965568 17552 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18058 17552 603 41 0 18017 0
vsize: 72232
[startup+810.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 18412 0 0 0 80948 68 0 0 25 0 1 0 487825525 75710464 17964 4294967295 134512640 134672761 3221224624 3221223808 134559575 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18484 17964 603 41 0 18443 0
vsize: 73936
[startup+820.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 18947 0 0 0 81946 70 0 0 25 0 1 0 487825525 77852672 18499 4294967295 134512640 134672761 3221224624 3221223808 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19007 18499 603 41 0 18966 0
vsize: 76028
[startup+830.174 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 19406 0 0 0 82945 72 0 0 25 0 1 0 487825525 79695872 18958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19457 18958 603 41 0 19416 0
vsize: 77828
[startup+840.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 19812 0 0 0 83943 74 0 0 25 0 1 0 487825525 81436672 19364 4294967295 134512640 134672761 3221224624 3221223728 134555256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19882 19364 603 41 0 19841 0
vsize: 79528
[startup+850.174 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 20167 0 0 0 84942 74 0 0 25 0 1 0 487825525 83419136 19719 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20366 19719 603 41 0 20325 0
vsize: 81464
[startup+860.173 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 20497 0 0 0 85941 76 0 0 25 0 1 0 487825525 84742144 20049 4294967295 134512640 134672761 3221224624 3221223708 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20689 20049 603 41 0 20648 0
vsize: 82756
[startup+870.174 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 20946 0 0 0 86940 77 0 0 25 0 1 0 487825525 86474752 20498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21112 20498 603 41 0 21071 0
vsize: 84448
[startup+880.175 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 21341 0 0 0 87939 79 0 0 25 0 1 0 487825525 88203264 20893 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21534 20893 603 41 0 21493 0
vsize: 86136
[startup+890.175 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 21615 0 0 0 88938 79 0 0 25 0 1 0 487825525 89276416 21167 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21796 21167 603 41 0 21755 0
vsize: 87184
[startup+900.176 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 22174 0 0 0 89937 81 0 0 25 0 1 0 487825525 91512832 21726 4294967295 134512640 134672761 3221224624 3221223824 134557885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22342 21726 603 41 0 22301 0
vsize: 89368
[startup+910.175 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 22424 0 0 0 90936 81 0 0 25 0 1 0 487825525 92565504 21976 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22599 21976 603 41 0 22558 0
vsize: 90396
[startup+920.176 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 22875 0 0 0 91935 83 0 0 25 0 1 0 487825525 94425088 22427 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23053 22427 603 41 0 23012 0
vsize: 92212
[startup+930.176 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 23275 0 0 0 92934 84 0 0 25 0 1 0 487825525 96010240 22827 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23440 22827 603 41 0 23399 0
vsize: 93760
[startup+940.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 23609 0 0 0 93933 85 0 0 25 0 1 0 487825525 97337344 23161 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23764 23161 603 41 0 23723 0
vsize: 95056
[startup+950.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 23904 0 0 0 94932 86 0 0 25 0 1 0 487825525 98525184 23456 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24054 23456 603 41 0 24013 0
vsize: 96216
[startup+960.177 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 24267 0 0 0 95931 87 0 0 25 0 1 0 487825525 100118528 23819 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24443 23819 603 41 0 24402 0
vsize: 97772
[startup+970.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 24627 0 0 0 96930 88 0 0 25 0 1 0 487825525 101580800 24179 4294967295 134512640 134672761 3221224624 3221223808 134559540 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24800 24179 603 41 0 24759 0
vsize: 99200
[startup+980.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 25001 0 0 0 97929 89 0 0 25 0 1 0 487825525 103051264 24553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25159 24553 603 41 0 25118 0
vsize: 100636
[startup+990.178 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 25349 0 0 0 98928 90 0 0 25 0 1 0 487825525 104505344 24901 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25514 24901 603 41 0 25473 0
vsize: 102056
[startup+1000.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 25847 0 0 0 99927 92 0 0 25 0 1 0 487825525 106516480 25399 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26005 25399 603 41 0 25964 0
vsize: 104020
[startup+1010.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 26339 0 0 0 100925 93 0 0 25 0 1 0 487825525 108498944 25891 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26489 25891 603 41 0 26448 0
vsize: 105956
[startup+1020.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 26850 0 0 0 101924 95 0 0 25 0 1 0 487825525 110604288 26402 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27003 26402 603 41 0 26962 0
vsize: 108012
[startup+1030.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 27382 0 0 0 102922 96 0 0 25 0 1 0 487825525 112746496 26934 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27526 26934 603 41 0 27485 0
vsize: 110104
[startup+1040.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 27788 0 0 0 103921 98 0 0 25 0 1 0 487825525 114454528 27340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27943 27340 603 41 0 27902 0
vsize: 111772
[startup+1050.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 28237 0 0 0 104921 99 0 0 25 0 1 0 487825525 116318208 27789 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28398 27789 603 41 0 28357 0
vsize: 113592
[startup+1060.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 28688 0 0 0 105919 100 0 0 25 0 1 0 487825525 118161408 28240 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28848 28240 603 41 0 28807 0
vsize: 115392
[startup+1070.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 29177 0 0 0 106919 101 0 0 25 0 1 0 487825525 120152064 28729 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29334 28729 603 41 0 29293 0
vsize: 117336
[startup+1080.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 29635 0 0 0 107917 103 0 0 25 0 1 0 487825525 122007552 29187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29787 29187 603 41 0 29746 0
vsize: 119148
[startup+1090.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 30093 0 0 0 108915 104 0 0 25 0 1 0 487825525 123854848 29645 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30238 29645 603 41 0 30197 0
vsize: 120952
[startup+1100.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 30526 0 0 0 109914 106 0 0 25 0 1 0 487825525 125575168 30078 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30658 30078 603 41 0 30617 0
vsize: 122632
[startup+1110.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 30964 0 0 0 110913 107 0 0 25 0 1 0 487825525 127426560 30516 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31110 30516 603 41 0 31069 0
vsize: 124440
[startup+1120.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 31445 0 0 0 111912 108 0 0 25 0 1 0 487825525 129425408 30997 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31598 30997 603 41 0 31557 0
vsize: 126392
[startup+1130.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 31874 0 0 0 112911 109 0 0 25 0 1 0 487825525 131137536 31426 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32016 31426 603 41 0 31975 0
vsize: 128064
[startup+1140.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 32229 0 0 0 113910 110 0 0 25 0 1 0 487825525 132591616 31781 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32371 31781 603 41 0 32330 0
vsize: 129484
[startup+1150.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 32429 0 0 0 114910 111 0 0 25 0 1 0 487825525 133390336 31981 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32566 31981 603 41 0 32525 0
vsize: 130264
[startup+1160.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 32570 0 0 0 115910 111 0 0 25 0 1 0 487825525 134053888 32122 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32728 32122 603 41 0 32687 0
vsize: 130912
[startup+1170.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 32935 0 0 0 116909 112 0 0 25 0 1 0 487825525 135512064 32487 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33084 32487 603 41 0 33043 0
vsize: 132336
[startup+1180.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 33194 0 0 0 117909 113 0 0 25 0 1 0 487825525 136585216 32746 4294967295 134512640 134672761 3221224624 3221223808 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33346 32746 603 41 0 33305 0
vsize: 133384
[startup+1190.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 33630 0 0 0 118907 114 0 0 25 0 1 0 487825525 138317824 33182 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33769 33182 603 41 0 33728 0
vsize: 135076
[startup+1200.18 s]
Raw data (loadavg): 1.00 0.97 0.92 2/54 1259
Raw data (stat): 1259 (minisat+) R 1258 25347 25346 0 -1 0 34249 0 0 0 119906 116 0 0 25 0 1 0 487825525 140853248 33801 4294967295 134512640 134672761 3221224624 3221223796 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34388 33801 603 41 0 34347 0
vsize: 137552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.26 s]
Raw data (loadavg): 1.00 0.97 0.92 1/54 1259
Raw data (stat): 1259 (minisat+) Z 1258 25347 25346 0 -1 12 34252 0 0 0 119907 122 0 0 25 0 1 0 487825525 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.26
CPU time (s): 1200.3
CPU user time (s): 1199.07
CPU system time (s): 1.22781
CPU usage (%): 100.003
Max. virtual memory (Kb): 137552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####