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 15299

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        804564 kB
Buffers:          4936 kB
Cached:         197604 kB
SwapCached:        168 kB
Active:          23368 kB
Inactive:       182448 kB
HighTotal:      131008 kB
HighFree:        50568 kB
LowTotal:       903652 kB
LowFree:        753996 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7220 kB
Slab:            18460 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:06:37 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 17992 7 1200.2 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 |  127883   429142 |   42627       0        0     nan |  0.000 % |
c |       100 |  127774   428867 |   46889      89      478     5.4 | 12.479 % |
c |       252 |  127329   427816 |   51578     207     3447    16.7 | 12.947 % |
c |       477 |  127297   427712 |   56736     426     5916    13.9 | 12.969 % |
c |       814 |  127297   427712 |   62410     763    27661    36.3 | 12.969 % |
c |      1321 |  127117   427196 |   68651    1247    43670    35.0 | 13.109 % |
c |      2080 |  127086   427126 |   75516    2005    78307    39.1 | 13.138 % |
c |      3220 |  127010   426955 |   83067    3143   128814    41.0 | 13.210 % |
c |      4929 |  126832   426521 |   91374    4837   182334    37.7 | 13.390 % |
c |      7494 |  126173   424903 |  100512    7328   248950    34.0 | 14.035 % |
c |     11338 |  126065   424621 |  110563   11165   394784    35.4 | 14.121 % |
c |     17106 |  125035   422180 |  121619   16825   666033    39.6 | 15.180 % |
c |     25755 |  123957   419539 |  133781   25178  1207532    48.0 | 16.264 % |
c |     38730 |  123112   417392 |  147159   37914  2085846    55.0 | 17.099 % |
c |     58195 |  122691   416311 |  161875   57286  3215580    56.1 | 17.506 % |
c |     87387 |  122161   414707 |  178063   85947  5339297    62.1 | 17.863 % |
c ==============================================================================
c [1mFound solution: 1271200[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 |    100616 |  121401   412245 |   40467   99029  6613097    66.8 | 17.863 % |
c |    100717 |  121387   412206 |   44513   23194  1367463    59.0 | 18.263 % |
c |    100867 |  121387   412206 |   48965   23344  1373055    58.8 | 18.263 % |
c |    101093 |  121387   412206 |   53861   23570  1379940    58.5 | 18.263 % |
c |    101432 |  121387   412206 |   59247   23909  1387918    58.1 | 18.263 % |
c |    101938 |  121383   412197 |   65172   24414  1416907    58.0 | 18.267 % |
c |    102697 |  121378   412182 |   71689   25172  1457794    57.9 | 18.271 % |
c |    103836 |  121368   412152 |   78858   26306  1530200    58.2 | 18.278 % |
c |    105544 |  121368   412152 |   86744   28014  1647782    58.8 | 18.278 % |
c |    108108 |  121281   411878 |   95419   30565  1909263    62.5 | 18.321 % |
c |    111952 |  121260   411811 |  104960   34406  2136305    62.1 | 18.332 % |
c |    117721 |  121041   411103 |  115457   40159  2524367    62.9 | 18.440 % |
c |    126370 |  120860   410553 |  127002   48767  3105845    63.7 | 18.551 % |
c |    139344 |  120035   408172 |  139703   61599  4206150    68.3 | 19.203 % |
c ==============================================================================
c [1mFound solution: 1263104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    149931 |  119752   407372 |   39917   72004  5277914    73.3 | 19.203 % |
c |    150031 |  119752   407372 |   43908   23684  1309524    55.3 | 19.450 % |
c |    150182 |  119740   407330 |   48299   23833  1314857    55.2 | 19.454 % |
c |    150410 |  119740   407330 |   53129   24061  1328525    55.2 | 19.454 % |
c |    150749 |  119740   407330 |   58442   24400  1350090    55.3 | 19.454 % |
c |    151255 |  119740   407330 |   64286   24906  1371827    55.1 | 19.454 % |
c |    152015 |  119740   407330 |   70715   25666  1431970    55.8 | 19.454 % |
c |    153154 |  119740   407330 |   77786   26805  1459023    54.4 | 19.454 % |
c |    154864 |  119656   407131 |   85565   27479  1516140    55.2 | 19.565 % |
c |    157426 |  119651   407116 |   94122   30040  1700311    56.6 | 19.569 % |
c |    161270 |  119651   407116 |  103534   33884  1813500    53.5 | 19.569 % |
c |    167036 |  119576   406922 |  113887   39636  2276479    57.4 | 19.644 % |
c |    175685 |  119494   406704 |  125276   48271  3142550    65.1 | 19.716 % |
c |    188659 |  119084   405545 |  137804   60046  4300444    71.6 | 20.040 % |
c ==============================================================================
c [1mFound solution: 1241440[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 |    194969 |  119107   405596 |   39702   66355  5129226    77.3 | 20.040 % |
c |    195069 |  119092   405545 |   43672   22792  1475939    64.8 | 20.048 % |
c |    195221 |  119092   405545 |   48039   22944  1482378    64.6 | 20.048 % |
c |    195450 |  119092   405545 |   52843   23173  1498494    64.7 | 20.048 % |
c |    195787 |  119092   405545 |   58127   23510  1516047    64.5 | 20.048 % |
c |    196293 |  119083   405514 |   63940   24011  1542162    64.2 | 20.052 % |
c |    197055 |  119078   405499 |   70334   24771  1607915    64.9 | 20.055 % |
c |    198196 |  119024   405317 |   77367   25902  1695732    65.5 | 20.077 % |
c |    199904 |  119024   405317 |   85104   27610  1870366    67.7 | 20.077 % |
c |    202466 |  118854   404727 |   93615   30151  2184119    72.4 | 20.135 % |
c |    206312 |  118768   404509 |  102976   33994  2435800    71.7 | 20.235 % |
c |    212080 |  118662   404170 |  113274   39742  2882843    72.5 | 20.300 % |
c |    220731 |  118027   402015 |  124601   48310  3743893    77.5 | 20.574 % |
c |    233705 |  118001   401934 |  137062   61279  5269441    86.0 | 20.588 % |
c |    253169 |  117742   401137 |  150768   80718  7906303    97.9 | 20.746 % |
c |    282361 |  116265   396135 |  165845  109691 11065517   100.9 | 21.495 % |
c |    326151 |  115387   393285 |  182429  153244 16517596   107.8 | 21.991 % |
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 -x9_bit6 -x9_b#### 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.85 0.91 0.90 2/56 19520
Raw data (stat): 19520 (runsolver) R 19519 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 426873119 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.88 0.91 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 1062 0 0 0 997 2 0 0 25 0 1 0 426873119 4886528 749 4294967295 134512640 134672761 3221224560 3221222400 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1193 749 603 41 0 1152 0
vsize: 4772
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.92 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 3751 0 0 0 1990 9 0 0 25 0 1 0 426873119 15982592 3303 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3902 3303 603 41 0 3861 0
vsize: 15608
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.92 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 3926 0 0 0 2990 9 0 0 25 0 1 0 426873119 16654336 3478 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4066 3478 603 41 0 4025 0
vsize: 16264
[startup+40.0015 s]
Raw data (loadavg): 0.92 0.92 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 4229 0 0 0 3988 11 0 0 25 0 1 0 426873119 17989632 3781 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4392 3781 603 41 0 4351 0
vsize: 17568
[startup+50.0023 s]
Raw data (loadavg): 0.93 0.92 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 4475 0 0 0 4988 12 0 0 25 0 1 0 426873119 19062784 4027 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4654 4027 603 41 0 4613 0
vsize: 18616
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.92 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 4736 0 0 0 5987 13 0 0 25 0 1 0 426873119 19996672 4288 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4882 4288 603 41 0 4841 0
vsize: 19528
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.93 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 5012 0 0 0 6986 13 0 0 25 0 1 0 426873119 21209088 4564 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5178 4564 603 41 0 5137 0
vsize: 20712
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.93 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 5353 0 0 0 7985 14 0 0 25 0 1 0 426873119 22544384 4905 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5504 4905 603 41 0 5463 0
vsize: 22016
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.93 0.90 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 5647 0 0 0 8984 15 0 0 25 0 1 0 426873119 23740416 5199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5796 5199 603 41 0 5755 0
vsize: 23184
[startup+100.003 s]
Raw data (loadavg): 0.97 0.93 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 5957 0 0 0 9983 17 0 0 25 0 1 0 426873119 25075712 5509 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6122 5509 603 41 0 6081 0
vsize: 24488
[startup+110.004 s]
Raw data (loadavg): 0.97 0.93 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 6202 0 0 0 10983 17 0 0 25 0 1 0 426873119 26136576 5754 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6381 5754 603 41 0 6340 0
vsize: 25524
[startup+120.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 6484 0 0 0 11982 18 0 0 25 0 1 0 426873119 27209728 6036 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6643 6036 603 41 0 6602 0
vsize: 26572
[startup+130.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 6852 0 0 0 12981 20 0 0 25 0 1 0 426873119 28667904 6404 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6999 6404 603 41 0 6958 0
vsize: 27996
[startup+140.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 7152 0 0 0 13980 21 0 0 25 0 1 0 426873119 30007296 6704 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7326 6704 603 41 0 7285 0
vsize: 29304
[startup+150.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 7403 0 0 0 14978 23 0 0 25 0 1 0 426873119 30949376 6955 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7556 6955 603 41 0 7515 0
vsize: 30224
[startup+160.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 7639 0 0 0 15977 23 0 0 25 0 1 0 426873119 31883264 7191 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7784 7191 603 41 0 7743 0
vsize: 31136
[startup+170.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 7893 0 0 0 16976 25 0 0 25 0 1 0 426873119 32948224 7445 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8044 7445 603 41 0 8003 0
vsize: 32176
[startup+180.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 8121 0 0 0 17976 25 0 0 25 0 1 0 426873119 34136064 7673 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8334 7673 603 41 0 8293 0
vsize: 33336
[startup+190.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 8389 0 0 0 18975 26 0 0 25 0 1 0 426873119 35201024 7941 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8594 7941 603 41 0 8553 0
vsize: 34376
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19520
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 8679 0 0 0 19974 27 0 0 25 0 1 0 426873119 36392960 8231 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8885 8231 603 41 0 8844 0
vsize: 35540
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 9019 0 0 0 20973 28 0 0 25 0 1 0 426873119 37740544 8571 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9214 8571 603 41 0 9173 0
vsize: 36856
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 9253 0 0 0 21972 29 0 0 25 0 1 0 426873119 38674432 8805 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9442 8805 603 41 0 9401 0
vsize: 37768
[startup+230.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 9636 0 0 0 22971 31 0 0 25 0 1 0 426873119 40280064 9188 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9834 9188 603 41 0 9793 0
vsize: 39336
[startup+240.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 9973 0 0 0 23970 32 0 0 25 0 1 0 426873119 41615360 9525 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10160 9525 603 41 0 10119 0
vsize: 40640
[startup+250.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 10350 0 0 0 24970 33 0 0 25 0 1 0 426873119 43216896 9902 4294967295 134512640 134672761 3221224560 3221223808 134562614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10551 9902 603 41 0 10510 0
vsize: 42204
[startup+260.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 10626 0 0 0 25968 34 0 0 25 0 1 0 426873119 44290048 10178 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10813 10178 603 41 0 10772 0
vsize: 43252
[startup+270.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 10866 0 0 0 26968 34 0 0 25 0 1 0 426873119 45223936 10418 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11041 10418 603 41 0 11000 0
vsize: 44164
[startup+280.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 10975 0 0 0 27968 34 0 0 25 0 1 0 426873119 45756416 10527 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11171 10527 603 41 0 11130 0
vsize: 44684
[startup+290.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11082 0 0 0 28967 35 0 0 25 0 1 0 426873119 46153728 10634 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11268 10634 603 41 0 11227 0
vsize: 45072
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 29966 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+310.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 30966 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+320.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 31967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+330.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 32967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+340.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 33967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+350.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 34967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+360.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 35967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+370.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 36967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+380.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 37967 37 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+390.012 s]
Raw data (loadavg): 1.07 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 38967 38 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+400.012 s]
Raw data (loadavg): 1.06 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 39967 38 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+410.012 s]
Raw data (loadavg): 1.05 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 40967 38 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+420.025 s]
Raw data (loadavg): 1.04 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 41968 38 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+430.038 s]
Raw data (loadavg): 1.03 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11302 0 0 0 42969 38 0 0 25 0 1 0 426873119 47095808 10854 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10854 603 41 0 11457 0
vsize: 45992
[startup+440.038 s]
Raw data (loadavg): 1.03 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11330 0 0 0 43969 38 0 0 25 0 1 0 426873119 47321088 10882 4294967295 134512640 134672761 3221224560 3221223860 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10882 603 41 0 11512 0
vsize: 46212
[startup+450.038 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11330 0 0 0 44966 39 0 0 25 0 1 0 426873119 47321088 10882 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10882 603 41 0 11512 0
vsize: 46212
[startup+460.05 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11330 0 0 0 45968 39 0 0 25 0 1 0 426873119 47321088 10882 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10882 603 41 0 11512 0
vsize: 46212
[startup+470.05 s]
Raw data (loadavg): 1.02 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11330 0 0 0 46968 39 0 0 25 0 1 0 426873119 47321088 10882 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10882 603 41 0 11512 0
vsize: 46212
[startup+480.053 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11330 0 0 0 47968 39 0 0 25 0 1 0 426873119 47321088 10882 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10882 603 41 0 11512 0
vsize: 46212
[startup+490.053 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11331 0 0 0 48968 39 0 0 25 0 1 0 426873119 47321088 10883 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10883 603 41 0 11512 0
vsize: 46212
[startup+500.053 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 19522
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11331 0 0 0 49968 39 0 0 25 0 1 0 426873119 47321088 10883 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10883 603 41 0 11512 0
vsize: 46212
[startup+510.053 s]
Raw data (loadavg): 1.01 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11331 0 0 0 50968 40 0 0 25 0 1 0 426873119 47321088 10883 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10883 603 41 0 11512 0
vsize: 46212
[startup+520.054 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11331 0 0 0 51968 40 0 0 25 0 1 0 426873119 47321088 10883 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10883 603 41 0 11512 0
vsize: 46212
[startup+530.061 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 52969 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+540.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 53971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+550.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 54971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+560.08 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 55971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+570.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 56971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+580.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 57971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+590.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 58971 40 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+600.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 59971 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+610.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 60971 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+620.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 61971 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+630.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 62971 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+640.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 63971 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+650.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11332 0 0 0 64972 41 0 0 25 0 1 0 426873119 47321088 10884 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10884 603 41 0 11512 0
vsize: 46212
[startup+660.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 65971 41 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+670.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 66971 41 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+680.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 67971 42 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+690.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 68972 42 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+700.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 69971 42 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+710.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11333 0 0 0 70971 42 0 0 25 0 1 0 426873119 47321088 10885 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11553 10885 603 41 0 11512 0
vsize: 46212
[startup+720.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 11641 0 0 0 71970 43 0 0 25 0 1 0 426873119 48513024 11193 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11844 11193 603 41 0 11803 0
vsize: 47376
[startup+730.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 12309 0 0 0 72968 46 0 0 25 0 1 0 426873119 51310592 11861 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12527 11861 603 41 0 12486 0
vsize: 50108
[startup+740.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 12642 0 0 0 73967 47 0 0 25 0 1 0 426873119 52633600 12194 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12850 12194 603 41 0 12809 0
vsize: 51400
[startup+750.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 12856 0 0 0 74967 47 0 0 25 0 1 0 426873119 53571584 12408 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13079 12408 603 41 0 13038 0
vsize: 52316
[startup+760.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 13219 0 0 0 75966 49 0 0 25 0 1 0 426873119 55037952 12771 4294967295 134512640 134672761 3221224560 3221223664 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13437 12771 603 41 0 13396 0
vsize: 53748
[startup+770.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 13339 0 0 0 76965 49 0 0 25 0 1 0 426873119 55435264 12891 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13534 12891 603 41 0 13493 0
vsize: 54136
[startup+780.082 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 13594 0 0 0 77964 50 0 0 25 0 1 0 426873119 56508416 13146 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13796 13146 603 41 0 13755 0
vsize: 55184
[startup+790.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 13841 0 0 0 78964 51 0 0 25 0 1 0 426873119 57585664 13393 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14059 13393 603 41 0 14018 0
vsize: 56236
[startup+800.081 s]
Raw data (loadavg): 1.00 0.98 0.91 2/56 19524
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 14046 0 0 0 79963 51 0 0 25 0 1 0 426873119 58392576 13598 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14256 13598 603 41 0 14215 0
vsize: 57024
[startup+810.081 s]
Raw data (loadavg): 1.08 1.00 0.92 2/60 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 14256 0 0 0 80962 52 0 0 25 0 1 0 426873119 59191296 13808 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14451 13808 603 41 0 14410 0
vsize: 57804
[startup+820.082 s]
Raw data (loadavg): 1.07 1.00 0.92 2/56 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 14532 0 0 0 81961 53 0 0 25 0 1 0 426873119 60399616 14084 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14746 14084 603 41 0 14705 0
vsize: 58984
[startup+830.082 s]
Raw data (loadavg): 1.06 1.00 0.92 2/56 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 14800 0 0 0 82961 54 0 0 25 0 1 0 426873119 61464576 14352 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14352 603 41 0 14965 0
vsize: 60024
[startup+840.082 s]
Raw data (loadavg): 1.05 1.00 0.92 2/56 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 15062 0 0 0 83960 55 0 0 25 0 1 0 426873119 62533632 14614 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15267 14614 603 41 0 15226 0
vsize: 61068
[startup+850.082 s]
Raw data (loadavg): 1.04 1.00 0.92 2/56 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 15312 0 0 0 84959 56 0 0 25 0 1 0 426873119 63614976 14864 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15531 14864 603 41 0 15490 0
vsize: 62124
[startup+860.082 s]
Raw data (loadavg): 1.03 1.00 0.92 2/56 19579
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 15679 0 0 0 85959 56 0 0 25 0 1 0 426873119 65093632 15231 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15892 15231 603 41 0 15851 0
vsize: 63568
[startup+870.082 s]
Raw data (loadavg): 1.03 1.00 0.92 2/56 19581
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 15995 0 0 0 86957 58 0 0 25 0 1 0 426873119 66281472 15547 4294967295 134512640 134672761 3221224560 3221223728 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16182 15547 603 41 0 16141 0
vsize: 64728
[startup+880.082 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 19581
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 16135 0 0 0 87957 58 0 0 25 0 1 0 426873119 66945024 15687 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16344 15687 603 41 0 16303 0
vsize: 65376
[startup+890.082 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 19583
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 16135 0 0 0 88958 58 0 0 25 0 1 0 426873119 66945024 15687 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16344 15687 603 41 0 16303 0
vsize: 65376
[startup+900.083 s]
Raw data (loadavg): 1.02 1.00 0.92 2/56 19583
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 16257 0 0 0 89957 58 0 0 25 0 1 0 426873119 67346432 15809 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16442 15809 603 41 0 16401 0
vsize: 65768
[startup+910.083 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 19583
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 16531 0 0 0 90957 59 0 0 25 0 1 0 426873119 68546560 16083 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16735 16083 603 41 0 16694 0
vsize: 66940
[startup+920.084 s]
Raw data (loadavg): 1.01 1.00 0.92 2/56 19583
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 16780 0 0 0 91957 60 0 0 25 0 1 0 426873119 69468160 16332 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16960 16332 603 41 0 16919 0
vsize: 67840
[startup+930.091 s]
Raw data (loadavg): 1.17 1.03 0.93 4/70 19600
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 17100 0 0 0 92954 60 0 0 25 0 1 0 426873119 70791168 16652 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17283 16652 603 41 0 17242 0
vsize: 69132
[startup+940.091 s]
Raw data (loadavg): 1.45 1.09 0.95 3/61 19615
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 17378 0 0 0 93954 61 0 0 25 0 1 0 426873119 71991296 16930 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17576 16930 603 41 0 17535 0
vsize: 70304
[startup+950.091 s]
Raw data (loadavg): 1.53 1.12 0.96 2/62 19859
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 17836 0 0 0 94945 64 0 0 25 0 1 0 426873119 73846784 17388 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18029 17388 603 41 0 17988 0
vsize: 72116
[startup+960.091 s]
Raw data (loadavg): 1.45 1.12 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 18197 0 0 0 95944 64 0 0 25 0 1 0 426873119 75325440 17749 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18390 17749 603 41 0 18349 0
vsize: 73560
[startup+970.091 s]
Raw data (loadavg): 1.38 1.11 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 18573 0 0 0 96943 66 0 0 25 0 1 0 426873119 76795904 18125 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18749 18125 603 41 0 18708 0
vsize: 74996
[startup+980.092 s]
Raw data (loadavg): 1.32 1.11 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 18899 0 0 0 97943 67 0 0 25 0 1 0 426873119 78131200 18451 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19075 18451 603 41 0 19034 0
vsize: 76300
[startup+990.092 s]
Raw data (loadavg): 1.27 1.11 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 19107 0 0 0 98942 67 0 0 25 0 1 0 426873119 79581184 18659 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19429 18659 603 41 0 19388 0
vsize: 77716
[startup+1000.09 s]
Raw data (loadavg): 1.23 1.10 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 19284 0 0 0 99942 68 0 0 25 0 1 0 426873119 80248832 18836 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19592 18836 603 41 0 19551 0
vsize: 78368
[startup+1010.09 s]
Raw data (loadavg): 1.19 1.10 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 19523 0 0 0 100941 69 0 0 25 0 1 0 426873119 81178624 19075 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19819 19075 603 41 0 19778 0
vsize: 79276
[startup+1020.09 s]
Raw data (loadavg): 1.16 1.10 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 19815 0 0 0 101941 69 0 0 25 0 1 0 426873119 82386944 19367 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20114 19367 603 41 0 20073 0
vsize: 80456
[startup+1030.09 s]
Raw data (loadavg): 1.14 1.09 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 20222 0 0 0 102940 70 0 0 25 0 1 0 426873119 84127744 19774 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20539 19774 603 41 0 20498 0
vsize: 82156
[startup+1040.09 s]
Raw data (loadavg): 1.12 1.09 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 20581 0 0 0 103939 71 0 0 25 0 1 0 426873119 85590016 20133 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20896 20133 603 41 0 20855 0
vsize: 83584
[startup+1050.09 s]
Raw data (loadavg): 1.10 1.08 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 20817 0 0 0 104939 72 0 0 25 0 1 0 426873119 86523904 20369 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21124 20369 603 41 0 21083 0
vsize: 84496
[startup+1060.09 s]
Raw data (loadavg): 1.08 1.08 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 20954 0 0 0 105938 72 0 0 25 0 1 0 426873119 87048192 20506 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21252 20506 603 41 0 21211 0
vsize: 85008
[startup+1070.09 s]
Raw data (loadavg): 1.07 1.08 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 21152 0 0 0 106938 73 0 0 25 0 1 0 426873119 87859200 20704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21450 20704 603 41 0 21409 0
vsize: 85800
[startup+1080.09 s]
Raw data (loadavg): 1.06 1.08 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 21568 0 0 0 107937 74 0 0 25 0 1 0 426873119 89579520 21120 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21870 21120 603 41 0 21829 0
vsize: 87480
[startup+1090.09 s]
Raw data (loadavg): 1.05 1.07 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 21762 0 0 0 108936 75 0 0 25 0 1 0 426873119 90386432 21314 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22067 21314 603 41 0 22026 0
vsize: 88268
[startup+1100.09 s]
Raw data (loadavg): 1.04 1.07 0.96 2/56 19902
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 21943 0 0 0 109935 76 0 0 25 0 1 0 426873119 91062272 21495 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22232 21495 603 41 0 22191 0
vsize: 88928
[startup+1110.09 s]
Raw data (loadavg): 1.03 1.07 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 22130 0 0 0 110934 77 0 0 25 0 1 0 426873119 91865088 21682 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22428 21682 603 41 0 22387 0
vsize: 89712
[startup+1120.1 s]
Raw data (loadavg): 1.03 1.06 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 22410 0 0 0 111934 78 0 0 25 0 1 0 426873119 93061120 21962 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22720 21962 603 41 0 22679 0
vsize: 90880
[startup+1130.1 s]
Raw data (loadavg): 1.02 1.06 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 22984 0 0 0 112933 79 0 0 25 0 1 0 426873119 95334400 22536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23275 22536 603 41 0 23234 0
vsize: 93100
[startup+1140.1 s]
Raw data (loadavg): 1.02 1.06 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 23449 0 0 0 113932 81 0 0 25 0 1 0 426873119 97185792 23001 4294967295 134512640 134672761 3221224560 3221223664 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23727 23001 603 41 0 23686 0
vsize: 94908
[startup+1150.1 s]
Raw data (loadavg): 1.02 1.06 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 23670 0 0 0 114931 81 0 0 25 0 1 0 426873119 98115584 23222 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23954 23222 603 41 0 23913 0
vsize: 95816
[startup+1160.1 s]
Raw data (loadavg): 1.01 1.05 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 23894 0 0 0 115931 82 0 0 25 0 1 0 426873119 99049472 23446 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24182 23446 603 41 0 24141 0
vsize: 96728
[startup+1170.1 s]
Raw data (loadavg): 1.01 1.05 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 24096 0 0 0 116930 83 0 0 25 0 1 0 426873119 99876864 23648 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24384 23648 603 41 0 24343 0
vsize: 97536
[startup+1180.1 s]
Raw data (loadavg): 1.01 1.05 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 24561 0 0 0 117929 84 0 0 25 0 1 0 426873119 101756928 24113 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24843 24113 603 41 0 24802 0
vsize: 99372
[startup+1190.1 s]
Raw data (loadavg): 1.01 1.05 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 25018 0 0 0 118928 86 0 0 25 0 1 0 426873119 103620608 24570 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25298 24570 603 41 0 25257 0
vsize: 101192
[startup+1200.1 s]
Raw data (loadavg): 1.01 1.05 0.96 2/56 19904
Raw data (stat): 19520 (minisat+) R 19519 12452 12451 0 -1 0 25277 0 0 0 119927 86 0 0 25 0 1 0 426873119 104689664 24829 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25559 24829 603 41 0 25518 0
vsize: 102236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.01 1.05 0.96 1/56 19904
Raw data (stat): 19520 (minisat+) Z 19519 12452 12451 0 -1 12 25280 0 0 0 119928 91 0 0 25 0 1 0 426873119 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.16
CPU time (s): 1200.2
CPU user time (s): 1199.29
CPU system time (s): 0.91486
CPU usage (%): 100.003
Max. virtual memory (Kb): 102236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####