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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-10teams.opb
MD5SUM	1ff3cc3253012886aa21be4feac6111e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	924
Optimality of the best value was proved	NO
Number of terms in the objective function	1800
Biggest coefficient in the objective function	86
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	41700
Number of bits of the sum of numbers in the objective function	16
Biggest number in a constraint	86
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	41700
Number of bits of the biggest sum of numbers	16
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.71
Number of variables	1800
Total number of constraints	2015
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2015
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	72
Trace number 16864

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        381120 kB
Buffers:         14900 kB
Cached:         615528 kB
SwapCached:          0 kB
Active:          30564 kB
Inactive:       602696 kB
HighTotal:      131008 kB
HighFree:        30044 kB
LowTotal:       903652 kB
LowFree:        351076 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            14660 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:08:34 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 12388 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 330 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 329]---> BDD-cost:  125
c ---[ 328]---> BDD-cost:  185
c ---[ 326]---> BDD-cost:   77
c ---[ 324]---> BDD-cost:   77
c ---[ 322]---> BDD-cost:   77
c ---[ 320]---> BDD-cost:   77
c ---[ 318]---> BDD-cost:   77
c ---[ 316]---> BDD-cost:   77
c ---[ 314]---> BDD-cost:   77
c ---[ 312]---> BDD-cost:   77
c ---[ 310]---> BDD-cost:   77
c ---[ 308]---> BDD-cost:   77
c ---[ 307]---> BDD-cost:  185
c ---[ 305]---> BDD-cost:   77
c ---[ 303]---> BDD-cost:   77
c ---[ 301]---> BDD-cost:   77
c ---[ 299]---> BDD-cost:   77
c ---[ 297]---> BDD-cost:   77
c ---[ 295]---> BDD-cost:   77
c ---[ 293]---> BDD-cost:   77
c ---[ 291]---> BDD-cost:   77
c ---[ 289]---> BDD-cost:   77
c ---[ 288]---> BDD-cost:  125
c ---[ 286]---> BDD-cost:   77
c ---[ 284]---> BDD-cost:   77
c ---[ 282]---> BDD-cost:   77
c ---[ 280]---> BDD-cost:   77
c ---[ 278]---> BDD-cost:   77
c ---[ 276]---> BDD-cost:   77
c ---[ 274]---> BDD-cost:   77
c ---[ 272]---> BDD-cost:   77
c ---[ 270]---> BDD-cost:   77
c ---[ 269]---> BDD-cost:  185
c ---[ 267]---> BDD-cost:   77
c ---[ 265]---> BDD-cost:   77
c ---[ 263]---> BDD-cost:   77
c ---[ 261]---> BDD-cost:   77
c ---[ 259]---> BDD-cost:   77
c ---[ 257]---> BDD-cost:   77
c ---[ 255]---> BDD-cost:   77
c ---[ 253]---> BDD-cost:   77
c ---[ 251]---> BDD-cost:   77
c ---[ 250]---> BDD-cost:  185
c ---[ 248]---> BDD-cost:   70
c ---[ 246]---> BDD-cost:   77
c ---[ 244]---> BDD-cost:   77
c ---[ 242]---> BDD-cost:   77
c ---[ 240]---> BDD-cost:   77
c ---[ 238]---> BDD-cost:   77
c ---[ 236]---> BDD-cost:   77
c ---[ 234]---> BDD-cost:   77
c ---[ 233]---> BDD-cost:  185
c ---[ 231]---> BDD-cost:   77
c ---[ 229]---> BDD-cost:   77
c ---[ 227]---> BDD-cost:   77
c ---[ 225]---> BDD-cost:   77
c ---[ 223]---> BDD-cost:   77
c ---[ 221]---> BDD-cost:   77
c ---[ 219]---> BDD-cost:   77
c ---[ 217]---> BDD-cost:   77
c ---[ 216]---> BDD-cost:  185
c ---[ 214]---> BDD-cost:   70
c ---[ 212]---> BDD-cost:   77
c ---[ 210]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:   77
c ---[ 206]---> BDD-cost:   77
c ---[ 204]---> BDD-cost:   77
c ---[ 202]---> BDD-cost:   77
c ---[ 200]---> BDD-cost:   77
c ---[ 198]---> BDD-cost:   70
c ---[ 197]---> BDD-cost:  185
c ---[ 195]---> BDD-cost:   77
c ---[ 193]---> BDD-cost:   77
c ---[ 191]---> BDD-cost:   77
c ---[ 189]---> BDD-cost:   77
c ---[ 187]---> BDD-cost:   77
c ---[ 185]---> BDD-cost:   77
c ---[ 183]---> BDD-cost:   77
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   77
c ---[ 178]---> BDD-cost:  125
c ---[ 176]---> BDD-cost:   77
c ---[ 174]---> BDD-cost:   77
c ---[ 172]---> BDD-cost:   77
c ---[ 170]---> BDD-cost:   77
c ---[ 168]---> BDD-cost:   77
c ---[ 166]---> BDD-cost:   77
c ---[ 164]---> BDD-cost:   77
c ---[ 162]---> BDD-cost:   77
c ---[ 160]---> BDD-cost:   77
c ---[ 159]---> BDD-cost:  185
c ---[ 157]---> BDD-cost:   77
c ---[ 155]---> BDD-cost:   77
c ---[ 153]---> BDD-cost:   77
c ---[ 151]---> BDD-cost:   77
c ---[ 149]---> BDD-cost:   77
c ---[ 147]---> BDD-cost:   77
c ---[ 145]---> BDD-cost:   77
c ---[ 143]---> BDD-cost:   77
c ---[ 141]---> BDD-cost:   77
c ---[ 140]---> BDD-cost:  185
c ---[ 139]---> BDD-cost:  185
c ---[ 137]---> BDD-cost:   77
c ---[ 135]---> BDD-cost:   77
c ---[ 133]---> BDD-cost:   77
c ---[ 131]---> BDD-cost:   77
c ---[ 129]---> BDD-cost:   77
c ---[ 127]---> BDD-cost:   77
c ---[ 125]---> BDD-cost:   77
c ---[ 123]---> BDD-cost:   77
c ---[ 121]---> BDD-cost:   77
c ---[ 120]---> BDD-cost:  178
c ---[ 118]---> BDD-cost:   77
c ---[ 116]---> BDD-cost:   77
c ---[ 114]---> BDD-cost:   77
c ---[ 112]---> BDD-cost:   77
c ---[ 110]---> BDD-cost:   77
c ---[ 108]---> BDD-cost:   77
c ---[ 106]---> BDD-cost:   77
c ---[ 104]---> BDD-cost:   77
c ---[ 102]---> BDD-cost:   77
c ---[ 101]---> BDD-cost:  185
c ---[  99]---> BDD-cost:   77
c ---[  97]---> BDD-cost:   77
c ---[  95]---> BDD-cost:   77
c ---[  93]---> BDD-cost:   77
c ---[  91]---> BDD-cost:   77
c ---[  89]---> BDD-cost:   77
c ---[  87]---> BDD-cost:   77
c ---[  85]---> BDD-cost:   77
c ---[  83]---> BDD-cost:   77
c ---[  82]---> BDD-cost:  125
c ---[  80]---> BDD-cost:   77
c ---[  79]---> BDD-cost:  185
c ---[  78]---> BDD-cost:  185
c ---[  77]---> BDD-cost:  178
c ---[  76]---> BDD-cost:  185
c ---[  75]---> BDD-cost:  185
c ---[  74]---> BDD-cost:  125
c ---[  73]---> BDD-cost:  185
c ---[  72]---> BDD-cost:  185
c ---[  71]---> BDD-cost:  178
c ---[  70]---> BDD-cost:  185
c ---[  69]---> BDD-cost:  185
c ---[  68]---> BDD-cost:  125
c ---[  67]---> BDD-cost:  185
c ---[  66]---> BDD-cost:  178
c ---[  65]---> BDD-cost:  185
c ---[  64]---> BDD-cost:  185
c ---[  63]---> BDD-cost:  185
c ---[  62]---> BDD-cost:  185
c ---[  61]---> BDD-cost:  125
c ---[  60]---> BDD-cost:  118
c ---[  59]---> BDD-cost:  185
c ---[  58]---> BDD-cost:  185
c ---[  57]---> BDD-cost:  185
c ---[  56]---> BDD-cost:  185
c ---[  55]---> BDD-cost:  178
c ---[  54]---> BDD-cost:  185
c ---[  53]---> BDD-cost:  185
c ---[  52]---> BDD-cost:  185
c ---[  51]---> BDD-cost:  185
c ---[  50]---> BDD-cost:  125
c ---[  49]---> BDD-cost:   76
c ---[  48]---> BDD-cost:   76
c ---[  47]---> BDD-cost:   76
c ---[  46]---> BDD-cost:   76
c ---[  45]---> BDD-cost:   76
c ---[  44]---> BDD-cost:   76
c ---[  43]---> BDD-cost:   76
c ---[  42]---> BDD-cost:   76
c ---[  41]---> BDD-cost:  177
c ---[  40]---> BDD-cost:   77
c ---[  39]---> BDD-cost:   77
c ---[  38]---> BDD-cost:   77
c ---[  37]---> BDD-cost:   77
c ---[  36]---> BDD-cost:   77
c ---[  35]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   77
c ---[  33]---> BDD-cost:   77
c ---[  32]---> BDD-cost:  123
c ---[  31]---> BDD-cost:   77
c ---[  30]---> BDD-cost:   77
c ---[  29]---> BDD-cost:   77
c ---[  28]---> BDD-cost:   77
c ---[  27]---> BDD-cost:   77
c ---[  26]---> BDD-cost:   77
c ---[  25]---> BDD-cost:   77
c ---[  24]---> BDD-cost:   77
c ---[  23]---> BDD-cost:   77
c ---[  22]---> BDD-cost:  183
c ---[  21]---> BDD-cost:   77
c ---[  20]---> BDD-cost:   77
c ---[  19]---> BDD-cost:   77
c ---[  18]---> BDD-cost:   77
c ---[  17]---> BDD-cost:   77
c ---[  16]---> BDD-cost:   77
c ---[  15]---> BDD-cost:   77
c ---[  14]---> BDD-cost:   75
c ---[  13]---> BDD-cost:   77
c ---[  12]---> BDD-cost:  183
c ---[  11]---> BDD-cost:   77
c ---[  10]---> BDD-cost:   77
c ---[   9]---> BDD-cost:   77
c ---[   8]---> BDD-cost:   77
c ---[   7]---> BDD-cost:   77
c ---[   6]---> BDD-cost:   77
c ---[   4]---> BDD-cost:   77
c ---[   2]---> BDD-cost:   77
c ---[   0]---> BDD-cost:   77
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   53221   141547 |   17740       0        0     nan |  0.000 % |
c |       100 |   53221   141547 |   19514     100     2449    24.5 |  1.808 % |
c |       251 |   53221   141547 |   21465     251    20371    81.2 |  1.808 % |
c |       476 |   53221   141547 |   23611     476    41787    87.8 |  1.808 % |
c |       813 |   53221   141547 |   25973     813    88284   108.6 |  1.808 % |
c ==============================================================================
c [1mFound solution: 1004[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:437446     Base: 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1052 | 1166927  2740854 |  388975    1052   103950    98.8 |  1.808 % |
c |      1152 | 1166692  2740324 |  427872    1150   104903    91.2 |  0.110 % |
c |      1303 | 1165913  2738556 |  470659    1297   115030    88.7 |  0.160 % |
c |      1529 | 1165913  2738556 |  517725    1523   140895    92.5 |  0.160 % |
c |      1866 | 1163093  2732109 |  569498    1845   171335    92.9 |  0.351 % |
c |      2372 | 1156871  2717831 |  626448    2323   209933    90.4 |  0.786 % |
c |      3131 | 1156871  2717831 |  689092    3082   347337   112.7 |  0.786 % |
c |      4272 | 1153690  2710526 |  758002    4177   521146   124.8 |  1.008 % |
c |      5981 | 1152860  2708620 |  833802    5882   872681   148.4 |  1.066 % |
c ==============================================================================
c [1mFound solution: 972[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7246 | 1144269  2689359 |  381423    7060  1064425   150.8 |  1.066 % |
c |      7347 | 1143890  2688494 |  419565    7159  1068556   149.3 |  1.950 % |
c |      7499 | 1143890  2688494 |  461521    7311  1079979   147.7 |  1.950 % |
c |      7724 | 1143890  2688494 |  507674    7536  1104489   146.6 |  1.950 % |
c |      8061 | 1143890  2688494 |  558441    7873  1132921   143.9 |  1.950 % |
c |      8572 | 1143890  2688494 |  614285    8384  1247968   148.9 |  1.950 % |
c |      9331 | 1143298  2687131 |  675714    9142  1396715   152.8 |  1.992 % |
c |     10470 | 1136577  2671642 |  743285   10252  1414890   138.0 |  2.472 % |
c |     12179 | 1136577  2671642 |  817614   11961  1449791   121.2 |  2.472 % |
c |     14744 | 1128930  2654014 |  899375   14468  2040174   141.0 |  3.022 % |
c |     18589 | 1128729  2653556 |  989313   18312  2941572   160.6 |  3.035 % |
c |     24356 | 1128729  2653556 | 1088244   24079  4605375   191.3 |  3.035 % |
c |     33006 | 1115986  2624171 | 1197068   32663  5554639   170.1 |  3.951 % |
c |     45980 | 1107698  2605032 | 1316775   45592 10091771   221.3 |  4.557 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x226_bit0 -x227_bit0 -x228_bit0 -x229_bit0 -x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 -x237_bit0 -x238_bit0 -x239_bit0 -x240_bit0 -x241_bit0 -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 -x303_bit0 -x304_bit0 -x305_bit0 -x306_bit0 -x307_bit0 x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 -x313_bit0 -x314_bit0 -x315_bit0 -x316_bit0 -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 -x557_bit0 -x558_bit0 -x559_bit0 -x560_bit0 -x561_bit0 -x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 x577_bit0 -x578_bit0 -x579_bit0 -x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 -x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 -x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 -x605_bit0 -x606_bit0 -x607_bit0 -x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 -x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 -x621_bit0 -x622_bit0 -x623_bit0 -x624_bit0 -x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 -x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 -x640_bit0 -x641_bit0 x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 -x648_bit0 -x649_bit0 -x650_bit0 -x651_bit0 -x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 -x667_bit0 -x668_bit0 -x669_bit0 -x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 -x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 -x684_bit0 -x685_bit0 -x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 -x693_bit0 -x694_bit0 -x695_bit0 -x696_bit0 -x697_bit0 -x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 -x709_bit0 -x710_bit0 -x711_bit0 -x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 -x726_bit0 -x727_bit0 -x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 -x735_bit0 -x736_bit0 -x737_bit0 -x738_bit0 x739_bit0 -x740_bit0 -x741_bit0 -x742_bit0 -x743_bit0 -x744_bit0 -x745_bit0 -x746_bit0 -x747_bit0 -x748_bit0 -x749_bit0 -x750_bit0 -x751_bit0 -x752_bit0 -x753_bit0 -x754_bit0 -x755_bit0 -x756_bit0 -x757_bit0 -x758_bit0 -x759_bit0 -x760_bit0 -x761_bit0 -x762_bit0 -x763_bit0 -x764_bit0 -x765_bit0 -x766_bit0 -x767_bit0 -x768_bit0 -x769_bit0 -x770_bit0 -x771_bit0 -x772_bit0 -x773_bit0 -x774_bit0 -x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 -x785_bit0 -x786_bit0 -x787_bit0 x788_bit0 -x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 -x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 -x801_bit0 -x802_bit0 -x803_bit0 -x804_bit0 -x805_bit0 -x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 -x812_bit0 -x813_bit0 -x814_bit0 -x815_bit0 -x816_bit0 -x817_bit0 -x818_bit0 -x819_bit0 -x820_bit0 -x821_bit0 -x822_bit0 -x823_bit0 -x824_bit0 -x825_bit0 -x826_bit0 -x827_bit0 -x828_bit0 -x829_bit0 -x830_bit0 -x831_bit0 -x832_bit0 -x833_bit0 -x834_bit0 -x835_bit0 -x836_bit0 -x837_bit0 -x838_bit0 x839_bit0 -x840_bit0 -x841_bit0 -x842_bit0 -x843_bit0 -x844_bit0 -x845_bit0 -x846_bit0 -x847_bit0 -x848_bit0 -x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 -x853_bit0 -x854_bit0 -x855_bit0 -x856_bit0 -x857_bit0 -x858_bit0 -x859_bit0 -x860_bit0 -x861_bit0 -x862_bit0 -x863_bit0 x864_bit0 -x865_bit0 -x866_bit0 -x867_bit0 -x868_bit0 -x869_bit0 -x870_bit0 -x871_bit0 -x872_bit0 -x873_bit0 -x874_bit0 -x875_bit0 -x876_bit0 -x877_bit0 -x878_bit0 -x879_bit0 -x880_bit0 -x881_bit0 -x882_bit0 -x883_bit0 -x884_bit0 -x885_bit0 -x886_bit0 -x887_bit0 -x888_bit0 -x889_bit0 -x890_bit0 -x891_bit0 -x892_bit0 -x893_bit0 -x894_bit0 -x895_bit0 -x896_bit0 -x897_bit0 -x898_bit0 -x899_bit0 -x900_bit0 -x901_bit0 -x902_bit0 -x903_bit0 -x904_bit0 -x905_bit0 -x906_bit0 -x907_bit0 -x908_bit0 -x909_bit0 -x910_bit0 -x911_bit0 -x912_bit0 -x913_bit0 -x914_bit0 -x915_bit0 -x916_bit0 -x917_bit0 -x918_bit0 -x919_bit0 -x920_bit0 -x921_bit0 -x922_bit0 -x923_bit0 -x924_bit0 -x925_bit0 -x926_bit0 -x927_bit0 -x928_bit0 -x929_bit0 -x930_bit0 -x931_bit0 -x932_bit0 -x933_bit0 -x934_bit0 -x935_bit0 -x936_bit0 -x937_bit0 -x938_bit0 -x939_bit0 -x940_bit0 x941_bit0 -x942_bit0 -x943_bit0 -x944_bit0 -x945_bit0 -x946_bit0 -x947_bit0 -x948_bit0 -x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 -x955_bit0 -x956_bit0 -x957_bit0 -x958_bit0 -x959_bit0 -x960_bit0 -x961_bit0 -x962_bit0 -x963_bit0 -x964_bit0 -x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 -x972_bit0 -x973_bit0 -x974_bit0 x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 -x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 -x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 -x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 -x1026_bit0 -x1027_bit0 -x1028_bit0 -x1029_bit0 -x1030_bit0 -x1031_bit0 -x1032_bit0 -x1033_bit0 -x1034_bit0 -x1035_bit0 -x1036_bit0 -x1037_bit0 -x1038_bit0 -x1039_bit0 -x1040_bit0 -x1041_bit0 -x1042_bit0 -x1043_bit0 -x1044_bit0 -x1045_bit0 -x1046_bit0 -x1047_bit0 x1048_bit0 -x1049_bit0 -x1050_bit0 -x1051_bit0 -x1052_bit0 -x1053_bit0 -x1054_bit0 -x1055_bit0 -x1056_bit0 -x1057_bit0 -x1058_bit0 -x1059_bit0 -x1060_bit0 -x1061_bit0 -x1062_bit0 -x1063_bit0 -x1064_bit0 -x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 -x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 -x1086_bit0 -x1087_bit0 -x1088_bit0 -x1089_bit0 -x1090_bit0 -x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 -x1098_bit0 -x1099_bit0 -x1100_bit0 -x1101_bit0 -x1102_bit0 -x1103_bit0 -x1104_bit0 x1105_bit0 -x1106_bit0 -x1107_bit0 -x1108_bit0 -x1109_bit0 -x1110_bit0 -x1111_bit0 -x1112_bit0 -x1113_bit0 -x1114_bit0 -x1115_bit0 -x1116_bit0 -x1117_bit0 -x1118_bit0 -x1119_bit0 -x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 -x1124_bit0 -x1125_bit0 -x1126_bit0 -x1127_bit0 -x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 -x1135_bit0 -x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 x1142_bit0 -x1143_bit0 -x1144_bit0 -x1145_bit0 -x1146_bit0 -x1147_bit0 -x1148_bit0 -x1149_bit0 -x1150_bit0 -x1151_bit0 -x1152_bit0 -x1153_bit0 -x1154_bit0 -x1155_bit0 -x1156_bit0 -x1157_bit0 -x1158_bit0 -x1159_bit0 -x1160_bit0 -x1161_bit0 -x1162_bit0 -x1163_bit0 -x1164_bit0 -x1165_bit0 -x1166_bit0 -x1167_bit0 -x1168_bit0 -x1169_bit0 -x1170_bit0 -x1171_bit0 -x1172_bit0 -x1173_bit0 -x1174_bit0 -x1175_bit0 -x1176_bit0 -x1177_bit0 -x1178_bit0 -x1179_bit0 -x1180_bit0 -x1181_bit0 -x1182_bit0 -x1183_bit0 -x1184_bit0 -x1185_bit0 -x1186_bit0 -x1187_bit0 -x1188_bit0 -x1189_bit0 -x1190_bit0 -x1191_bit0 -x1192_bit0 -x1193_bit0 -x1194_bit0 -x1195_bit0 -x1196_bit0 -x1197_bit0 -x1198_bit0 -x1199_bit0 -x1200_bit0 -x1201_bit0 -x1202_bit0 x1203_bit0 -x1204_bit0 -x1205_bit0 -x1206_bit0 -x1207_bit0 -x1208_bit0 -x1209_bit0 -x1210_bit0 -x1211_bit0 -x1212_bit0 -x1213_bit0 -x1214_bit0 -x1215_bit0 -x1216_bit0 -x1217_bit0 -x1218_bit0 -x1219_bit0 -x1220_bit0 -x1221_bit0 -x1222_bit0 -x1223_bit0 -x1224_bit0 -x1225_bit0 -x1226_bit0 -x1227_bit0 -x1228_bit0 -x1229_bit0 -x1230_bit0 -x1231_bit0 -x1232_bit0 -x1233_bit0 -x1234_bit0 -x1235_bit0 -x1236_bit0 -x1237_bit0 -x1238_bit0 -x1239_bit0 -x1240_bit0 -x1241_bit0 -x1242_bit0 -x1243_bit0 -x1244_bit0 -x1245_bit0 -x1246_bit0 -x1247_bit0 -x1248_bit0 -x1249_bit0 -x1250_bit0 -x1251_bit0 -x1252_bit0 -x1253_bit0 x1254_bit0 -x1255_bit0 -x1256_bit0 -x1257_bit0 -x1258_bit0 -x1259_bit0 -x1260_bit0 -x1261_bit0 -x1262_bit0 -x1263_bit0 -x1264_bit0 -x1265_bit0 -x1266_bit0 -x1267_bit0 -x1268_bit0 -x1269_bit0 -x1270_bit0 -x1271_bit0 -x1272_bit0 -x1273_bit0 x1274_bit0 -x1275_bit0 -x1276_bit0 -x1277_bit0 -x1278_bit0 -x1279_bit0 -x1280_bit0 -x1281_bit0 -x1282_bit0 -x1283_bit0 -x1284_bit0 -x1285_bit0 -x1286_bit0 -x1287_bit0 -x1288_bit0 -x1289_bit0 -x1290_bit0 -x1291_bit0 -x1292_bit0 -x1293_bit0 -x1294_bit0 -x1295_bit0 -x1296_bit0 -x1297_bit0 -x1298_bit0 -x1299_bit0 -x1300_bit0 -x1301_bit0 -x1302_bit0 -x1303_bit0 -x1304_bit0 -x1305_bit0 -x1306_bit0 -x1307_bit0 -x1308_bit0 -x1309_bit0 -x1310_bit0 -x1311_bit0 -x1312_bit0 -x1313_bit0 -x1314_bit0 -x1315_bit0 -x1316_bit0 -x1317_bit0 -x1318_bit0 -x1319_bit0 -x1320_bit0 -x1321_bit0 -x1322_bit0 -x1323_bit0 -x1324_bit0 -x1325_bit0 -x1326_bit0 x1327_bit0 -x1328_bit0 -x1329_bit0 -x1330_bit0 -x1331_bit0 -x1332_bit0 -x1333_bit0 -x1334_bit0 -x1335_bit0 -x1336_bit0 -x1337_bit0 -x1338_bit0 -x1339_bit0 -x1340_bit0 -x1341_bit0 -x1342_bit0 -x1343_bit0 -x1344_bit0 -x1345_bit0 -x1346_bit0 -x1347_bit0 -x1348_bit0 -x1349_bit0 -x1350_bit0 -x1351_bit0 -x1352_bit0 -x1353_bit0 -x1354_bit0 -x1355_bit0 -x1356_bit0 -x1357_bit0 -x1358_bit0 -x1359_bit0 -x1360_bit0 -x1361_bit0 -x1362_bit0 -x1363_bit0 -x1364_bit0 -x1365_bit0 -x1366_bit0 -x1367_bit0 -x1368_bit0 -x1369_bit0 -x1370_bit0 -x1371_bit0 -x1372_bit0 -x1373_bit0 -x1374_bit0 -x1375_bit0 -x1376_bit0 -x1377_bit0 -x1378_bit0 -x1379_bit0 -x1380_bit0 x1381_bit0 -x1382_bit0 -x1383_bit0 -x1384_bit0 -x1385_bit0 -x1386_bit0 -x1387_bit0 -x1388_bit0 -x1389_bit0 -x1390_bit0 -x1391_bit0 -x1392_bit0 -x1393_bit0 -x1394_bit0 -x1395_bit0 -x1396_bit0 -x1397_bit0 -x1398_bit0 -x1399_bit0 -x1400_bit0 -x1401_bit0 -x1402_bit0 -x1403_bit0 -x1404_bit0 -x1405_bit0 -x1406_bit0 -x1407_bit0 -x1408_bit0 -x1409_bit0 -x1410_bit0 -x1411_bit0 -x1412_bit0 -x1413_bit0 -x1414_bit0 -x1415_bit0 x1416_bit0 -x1417_bit0 -x1418_bit0 -x1419_bit0 -x1420_bit0 -x1421_bit0 -x1422_bit0 -x1423_bit0 -x1424_bit0 -x1425_bit0 -x1426_bit0 -x1427_bit0 -x1428_bit0 -x1429_bit0 -x1430_bit0 -x1431_bit0 -x1432_bit0 -x1433_bit0 -x1434_bit0 -x1435_bit0 -x1436_bit0 -x1437_bit0 -x1438_bit0 -x1439_bit0 -x1440_bit0 -x1441_bit0 -x1442_bit0 -x1443_bit0 -x1444_bit0 x1445_bit0 -x1446_bit0 -x1447_bit0 -x1448_bit0 -x1449_bit0 -x1450_bit0 -x1451_bit0 -x1452_bit0 -x1453_bit0 -x1454_bit0 -x1455_bit0 -x1456_bit0 -x1457_bit0 -x1458_bit0 -x1459_bit0 -x1460_bit0 -x1461_bit0 -x1462_bit0 -x1463_bit0 -x1464_bit0 -x1465_bit0 -x1466_bit0 -x1467_bit0 -x1468_bit0 -x1469_bit0 -x1470_bit0 -x1471_bit0 -x1472_bit0 -x1473_bit0 -x1474_bit0 -x1475_bit0 -x1476_bit0 -x1477_bit0 -x1478_bit0 -x1479_bit0 -x1480_bit0 -x1481_bit0 -x1482_bit0 -x1483_bit0 -x1484_bit0 -x1485_bit0 -x1486_bit0 -x1487_bit0 -x1488_bit0 -x1489_bit0 -x1490_bit0 -x1491_bit0 -x1492_bit0 -x1493_bit0 -x1494_bit0 -x1495_bit0 -x1496_bit0 -x1497_bit0 -x1498_bit0 -x1499_bit0 -x1500_bit0 -x1501_bit0 -x1502_bit0 -x1503_bit0 -x1504_bit0 -x1505_bit0 -x1506_bit0 -x1507_bit0 -x1508_bit0 -x1509_bit0 -x1510_bit0 -x1511_bit0 -x1512_bit0 -x1513_bit0 -x1514_bit0 -x1515_bit0 -x1516_bit0 -x1517_bit0 -x1518_bit0 -x1519_bit0 -x1520_bit0 -x1521_bit0 -x1522_bit0 -x1523_bit0 -x1524_bit0 -x1525_bit0 -x1526_bit0 -x1527_bit0 -x1528_bit0 x1529_bit0 -x1530_bit0 -x1531_bit0 -x1532_bit0 -x1533_bit0 -x1534_bit0 -x1535_bit0 -x1536_bit0 x1537_bit0 -x1538_bit0 -x1539_bit0 -x1540_bit0 -x1541_bit0 -x1542_bit0 -x1543_bit0 -x1544_bit0 -x1545_bit0 -x1546_bit0 -x1547_bit0 -x1548_bit0 -x1549_bit0 -x1550_bit0 -x1551_bit0 -x1552_bit0 -x1553_bit0 -x1554_bit0 -x1555_bit0 -x1556_bit0 -x1557_bit0 -x1558_bit0 -x1559_bit0 -x1560_bit0 -x1561_bit0 -x1562_bit0 -x1563_bit0 -x1564_bit0 -x1565_bit0 -x1566_bit0 -x1567_bit0 -x1568_bit0 -x1569_bit0 -x1570_bit0 -x1571_bit0 -x1572_bit0 -x1573_bit0 -x1574_bit0 -x1575_bit0 -x1576_bit0 -x1577_bit0 -x1578_bit0 x1579_bit0 -x1580_bit0 -x1581_bit0 -x1582_bit0 -x1583_bit0 -x1584_bit0 -x1585_bit0 -x1586_bit0 -x1587_bit0 -x1588_bit0 -x1589_bit0 -x1590_bit0 -x1591_bit0 -x1592_bit0 -x1593_bit0 -x1594_bit0 -x1595_bit0 -x1596_bit0 -x1597_bit0 -x1598_bit0 -x1599_bit0 -x1600_bit0 -x1601_bit0 -x1602_bit0 -x1603_bit0 -x1604_bit0 -x1605_bit0 -x1606_bit0 -x1607_bit0 -x1608_bit0 -x1609_bit0 -x1610_bit0 -x1611_bit0 -x1612_bit0 -x1613_bit0 -x1614_bit0 -x1615_bit0 -x1616_bit0 -x1617_bit0 -x1618_bit0 -x1619_bit0 -x1620_bit0 -x1621_bit0 -x1622_bit0 -x1623_bit0 -x1624_bit0 -x1625_bit0 -x1626_bit0 -x1627_bit0 -x1628_bit0 -x1629_bit0 -x1630_bit0 -x1631_bit0 -x1632_bit0 -x1633_bit0 -x1634_bit0 -x1635_bit0 -x1636_bit0 -x1637_bit0 -x1638_bit0 -x1639_bit0 -x1640_bit0 -x1641_bit0 -x1642_bit0 -x1643_bit0 -x1644_bit0 -x1645_bit0 x1646_bit0 -x1647_bit0 -x1648_bit0 -x1649_bit0 -x1650_bit0 -x1651_bit0 -x1652_bit0 -x1653_bit0 -x1654_bit0 -x1655_bit0 -x1656_bit0 -x1657_bit0 -x1658_bit0 -x1659_bit0 -x1660_bit0 -x1661_bit0 -x1662_bit0 -x1663_bit0 -x1664_bit0 -x1665_bit0 -x1666_bit0 -x1667_bit0 -x1668_bit0 -x1669_bit0 -x1670_bit0 -x1671_bit0 -x1672_bit0 -x1673_bit0 -x1674_bit0 -x1675_bit0 -x1676_bit0 -x1677_bit0 -x1678_bit0 -x1679_bit0 -x1680_bit0 -x1681_bit0 -x1682_bit0 -x1683_bit0 -x1684_bit0 -x1685_bit0 -x1686_bit0 -x1687_bit0 -x1688_bit0 -x1689_bit0 -x1690_bit0 -x1691_bit0 -x1692_bit0 -x1693_bit0 -x1694_bit0 -x1695_bit0 -x1696_bit0 -x1697_bit0 -x1698_bit0 x1699_bit0 -x1700_bit0 -x1701_bit0 -x1702_bit0 -x1703_bit0 -x1704_bit0 -x1705_bit0 -x1706_bit0 -x1707_bit0 -x1708_bit0 -x1709_bit0 -x1710_bit0 -x1711_bit0 -x1712_bit0 -x1713_bit0 -x1714_bit0 -x1715_bit0 -x1716_bit0 -x1717_bit0 -x1718_bit0 -x1719_bit0 -x1720_bit0 -x1721_bit0 -x1722_bit0 -x1723_bit0 -x1724_bit0 -x1725_bit0 -x1726_bit0 -x1727_bit0 -x1728_bit0 -x1729_bit0 -x1730_bit0 -x1731_bit0 -x1732_bit0 -x1733_bit0 -x1734_bit0 -x1735_bit0 -x1736_bit0 -x1737_bit0 -x1738_bit0 -x1739_bit0 -x1740_bit0 -x1741_bit0 -x1742_bit0 -x1743_bit0 -x1744_bit0 -x1745_bit0 -x1746_bit0 -x1747_bit0 -x1748_bit0 -x1749_bit0 -x1750_bit0 -x1751_bit0 -x1752_bit0 x1753_bit0 -x1754_bit0 -x1755_bit0 -x1756_bit0 -x1757_bit0 x1758_bit0 -x1759_bit0 -x1760_bit0 -x1761_bit0 -x1762_bit0 -x1763_bit0 -x1764_bit0 -x1765_bit0 -x1766_bit0 -x1767_bit0 -x1768_bit0 -x1769_bit0 -x1770_bit0 -x1771_bit0 -x1772_bit0 -x1773_bit0 -x1774_bit0 -x1775_bit0 -x1776_bit0 -x1777_bit0 -x1778_bit0 -x1779_bit0 -x1780_bit0 -x1781_bit0 -x1782_bit0 -x1783_bit0 -x1784_bit0 -x1785_bit0 -x1786_bit0 -x1787_bit0 -x1788_bit0 -x1789_bit0 -x1790_bit0 -x1791_bit0 -x1792_bit0 -x1793_bit0 -x1794_bit0 -x1795_bit0 -x1796_bit0 -x1797_bit0 -x1798_bit0 -x1799_bit0 -x1800_bit0 -x1801_bit0 -x1802_bit0 -x1803_bit0 -x1804_bit0 -x1805_bit0 -x1806_bit0 -x1807_bit0 -x1808_bit0 -x1809_bit0 -x1810_bit0 -x1811_bit0 -x1812_bit0 -x1813_bit0 -x1814_bit0 -x1815_bit0 -x1816_bit0 -x1817_bit0 -x1818_bit0 -x1819_bit0 -x1820_bit0 -x1821_bit0 -x1822_bit0 -x1823_bit0 -x1824_bit0 -x1825_bit0 -x1826_bit0 -x1827_bit0 -x1828_bit0 -x1829_bit0 -x1830_bit0 -x1831_bit0 -x1832_bit0 -x1833_bit0 -x1834_bit0 -x1835_bit0 x1836_bit0 -x1837_bit0 -x1838_bit0 -x1839_bit0 -x1840_bit0 -x1841_bit0 -x1842_bit0 -x1843_bit0 -x1844_bit0 -x1845_bit0 -x1846_bit0 -x1847_bit0 -x1848_bit0 -x1849_bit0 -x1850_bit0 -x1851_bit0 -x1852_bit0 -x1853_bit0 -x1854_bit0 -x1855_bit0 x1856_bit0 -x1857_bit0 -x1858_bit0 -x1859_bit0 -x1860_bit0 -x1861_bit0 -x1862_bit0 -x1863_bit0 -x1864_bit0 -x1865_bit0 -x1866_bit0 -x1867_bit0 -x1868_bit0 -x1869_bit0 -x1870_bit0 -x1871_bit0 -x1872_bit0 -x1873_bit0 -x1874_bit0 -x1875_bit0 -x1876_bit0 -x1877_bit0 -x1878_bit0 -x1879_bit0 -x1880_bit0 -x1881_bit0 -x1882_bit0 -x1883_bit0 -x1884_bit0 -x1885_bit0 -x1886_bit0 -x1887_bit0 -x1888_bit0 -x1889_bit0 -x1890_bit0 -x1891_bit0 -x1892_bit0 -x1893_bit0 -x1894_bit0 -x1895_bit0 -x1896_bit0 -x1897_bit0 -x1898_bit0 -x1899_bit0 -x1900_bit0 -x1901_bit0 -x1902_bit0 -x1903_bit0 -x1904_bit0 -x1905_bit0 -x1906_bit0 -x1907_bit0 x1908_bit0 -x1909_bit0 -x1910_bit0 -x1911_bit0 -x1912_bit0 -x1913_bit0 -x1914_bit0 -x1915_bit0 -x1916_bit0 -x1917_bit0 -x1918_bit0 -x1919_bit0 -x1920_bit0 -x1921_bit0 -x1922_bit0 -x1923_bit0 -x1924_bit0 -x1925_bit0 -x1926_bit0 -x1927_bit0 -x1928_bit0 -x1929_bit0 -x1930_bit0 -x1931_bit0 -x1932_bit0 -x1933_bit0 -x1934_bit0 -x1935_bit0 -x1936_bit0 -x1937_bit0 -x1938_bit0 -x1939_bit0 -x1940_bit0 -x1941_bit0 -x1942_bit0 x1943_bit0 -x1944_bit0 -x1945_bit0 -x1946_bit0 -x1947_bit0 -x1948_bit0 -x1949_bit0 -x1950_bit0 -x1951_bit0 -x1952_bit0 -x1953_bit0 -x1954_bit0 -x1955_bit0 -x1956_bit0 -x1957_bit0 -x1958_bit0 -x1959_bit0 -x1960_bit0 -x1961_bit0 -x1962_bit0 -x1963_bit0 -x1964_bit0 -x1965_bit0 -x1966_bit0 -x1967_bit0 -x1968_bit0 -x1969_bit0 -x1970_bit0 -x1971_bit0 -x1972_bit0 -x1973_bit0 -x1974_bit0 -x1975_bit0 -x1976_bit0 -x1977_bit0 -x1978_bit0 -x1979_bit0 -x1980_bit0 -x1981_bit0 -x1982_bit0 -x1983_bit0 -x1984_bit0 -x1985_bit0 -x1986_bit0 -x1987_bit0 -x1988_bit0 -x1989_bit0 -x1990_bit0 -x1991_bit0 -x1992_bit0 -x1993_bit0 -x1994_bit0 -x1995_bit0 -x1996_bit0 -#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.96 0.94 2/54 4881
Raw data (stat): 4881 (runsolver) R 4880 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 485535613 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.87 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 34780 0 0 0 920 78 0 0 25 0 1 0 485535613 152027136 33451 4294967295 134512640 134672761 3221224528 3221219256 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37116 33453 603 41 0 37075 0
vsize: 148464
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35323 0 0 0 1918 80 0 0 25 0 1 0 485535613 152838144 33994 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37314 33994 603 41 0 37273 0
vsize: 149256
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35405 0 0 0 2918 80 0 0 25 0 1 0 485535613 153112576 34076 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37381 34076 603 41 0 37340 0
vsize: 149524
[startup+40.0008 s]
Raw data (loadavg): 0.92 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35433 0 0 0 3918 80 0 0 25 0 1 0 485535613 153251840 34104 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37415 34104 603 41 0 37374 0
vsize: 149660
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35467 0 0 0 4918 80 0 0 25 0 1 0 485535613 153387008 34138 4294967295 134512640 134672761 3221224528 3221223676 1074732960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37448 34138 603 41 0 37407 0
vsize: 149792
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35552 0 0 0 5917 80 0 0 25 0 1 0 485535613 153788416 34223 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37546 34223 603 41 0 37505 0
vsize: 150184
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35619 0 0 0 6916 81 0 0 25 0 1 0 485535613 154058752 34290 4294967295 134512640 134672761 3221224528 3221223700 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37612 34290 603 41 0 37571 0
vsize: 150448
[startup+80.002 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35656 0 0 0 7916 81 0 0 25 0 1 0 485535613 154189824 34327 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37644 34327 603 41 0 37603 0
vsize: 150576
[startup+90.0018 s]
Raw data (loadavg): 0.96 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35795 0 0 0 8916 82 0 0 25 0 1 0 485535613 154726400 34466 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37775 34466 603 41 0 37734 0
vsize: 151100
[startup+100.002 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35898 0 0 0 9916 82 0 0 25 0 1 0 485535613 155127808 34569 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37873 34569 603 41 0 37832 0
vsize: 151492
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 35962 0 0 0 10916 82 0 0 25 0 1 0 485535613 155398144 34633 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37939 34633 603 41 0 37898 0
vsize: 151756
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36121 0 0 0 11915 83 0 0 25 0 1 0 485535613 156073984 34792 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38104 34792 603 41 0 38063 0
vsize: 152416
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36163 0 0 0 12916 83 0 0 25 0 1 0 485535613 156205056 34834 4294967295 134512640 134672761 3221224528 3221223732 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38136 34834 603 41 0 38095 0
vsize: 152544
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36164 0 0 0 13916 83 0 0 25 0 1 0 485535613 156205056 34835 4294967295 134512640 134672761 3221224528 3221223664 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38136 34835 603 41 0 38095 0
vsize: 152544
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36230 0 0 0 14916 83 0 0 25 0 1 0 485535613 156475392 34901 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38202 34901 603 41 0 38161 0
vsize: 152808
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36403 0 0 0 15915 84 0 0 25 0 1 0 485535613 157016064 35074 4294967295 134512640 134672761 3221224528 3221223652 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38334 35074 603 41 0 38293 0
vsize: 153336
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 36969 0 0 0 16913 85 0 0 25 0 1 0 485535613 160235520 35619 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39120 35619 603 41 0 39079 0
vsize: 156480
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37029 0 0 0 17913 85 0 0 25 0 1 0 485535613 160501760 35679 4294967295 134512640 134672761 3221224528 3221223676 1074733095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39185 35679 603 41 0 39144 0
vsize: 156740
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37142 0 0 0 18913 86 0 0 25 0 1 0 485535613 160923648 35792 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39288 35792 603 41 0 39247 0
vsize: 157152
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37217 0 0 0 19912 86 0 0 25 0 1 0 485535613 161329152 35867 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39387 35867 603 41 0 39346 0
vsize: 157548
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37308 0 0 0 20912 86 0 0 25 0 1 0 485535613 161599488 35958 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39453 35958 603 41 0 39412 0
vsize: 157812
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37314 0 0 0 21912 86 0 0 25 0 1 0 485535613 161730560 35964 4294967295 134512640 134672761 3221224528 3221223700 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39485 35964 603 41 0 39444 0
vsize: 157940
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37325 0 0 0 22912 87 0 0 25 0 1 0 485535613 161730560 35975 4294967295 134512640 134672761 3221224528 3221223664 134560585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39485 35975 603 41 0 39444 0
vsize: 157940
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37356 0 0 0 23912 87 0 0 25 0 1 0 485535613 161865728 36006 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39518 36006 603 41 0 39477 0
vsize: 158072
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37434 0 0 0 24912 87 0 0 25 0 1 0 485535613 162131968 36084 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39583 36084 603 41 0 39542 0
vsize: 158332
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37602 0 0 0 25912 87 0 0 25 0 1 0 485535613 162807808 36252 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39748 36252 603 41 0 39707 0
vsize: 158992
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37747 0 0 0 26912 88 0 0 25 0 1 0 485535613 163475456 36397 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39911 36397 603 41 0 39870 0
vsize: 159644
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37894 0 0 0 27912 88 0 0 25 0 1 0 485535613 164012032 36544 4294967295 134512640 134672761 3221224528 3221223664 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40042 36544 603 41 0 40001 0
vsize: 160168
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 37988 0 0 0 28912 88 0 0 25 0 1 0 485535613 164417536 36638 4294967295 134512640 134672761 3221224528 3221223696 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40141 36638 603 41 0 40100 0
vsize: 160564
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38116 0 0 0 29912 89 0 0 25 0 1 0 485535613 164954112 36766 4294967295 134512640 134672761 3221224528 3221223632 134560483 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40272 36766 603 41 0 40231 0
vsize: 161088
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38289 0 0 0 30912 89 0 0 25 0 1 0 485535613 165621760 36939 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40435 36939 603 41 0 40394 0
vsize: 161740
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38435 0 0 0 31911 90 0 0 25 0 1 0 485535613 166309888 37085 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40603 37085 603 41 0 40562 0
vsize: 162412
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38547 0 0 0 32911 90 0 0 25 0 1 0 485535613 166715392 37197 4294967295 134512640 134672761 3221224528 3221223728 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40702 37197 603 41 0 40661 0
vsize: 162808
[startup+340.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38671 0 0 0 33911 91 0 0 25 0 1 0 485535613 167251968 37321 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40833 37321 603 41 0 40792 0
vsize: 163332
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38812 0 0 0 34910 91 0 0 25 0 1 0 485535613 167911424 37462 4294967295 134512640 134672761 3221224528 3221223632 134559969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40994 37462 603 41 0 40953 0
vsize: 163976
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 38893 0 0 0 35910 92 0 0 25 0 1 0 485535613 168181760 37543 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41060 37543 603 41 0 41019 0
vsize: 164240
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39029 0 0 0 36910 92 0 0 25 0 1 0 485535613 168722432 37679 4294967295 134512640 134672761 3221224528 3221223664 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41192 37679 603 41 0 41151 0
vsize: 164768
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39198 0 0 0 37909 93 0 0 25 0 1 0 485535613 169394176 37848 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41356 37848 603 41 0 41315 0
vsize: 165424
[startup+390.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39366 0 0 0 38909 93 0 0 25 0 1 0 485535613 170061824 38016 4294967295 134512640 134672761 3221224528 3221223676 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41519 38016 603 41 0 41478 0
vsize: 166076
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39535 0 0 0 39909 94 0 0 25 0 1 0 485535613 170737664 38185 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41684 38185 603 41 0 41643 0
vsize: 166736
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39715 0 0 0 40908 94 0 0 25 0 1 0 485535613 171544576 38365 4294967295 134512640 134672761 3221224528 3221223696 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41881 38365 603 41 0 41840 0
vsize: 167524
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 39903 0 0 0 41908 95 0 0 25 0 1 0 485535613 172351488 38553 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42078 38553 603 41 0 42037 0
vsize: 168312
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40080 0 0 0 42908 95 0 0 25 0 1 0 485535613 173023232 38730 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42242 38730 603 41 0 42201 0
vsize: 168968
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40281 0 0 0 43907 96 0 0 25 0 1 0 485535613 173830144 38931 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42439 38931 603 41 0 42398 0
vsize: 169756
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40457 0 0 0 44907 96 0 0 25 0 1 0 485535613 174497792 39107 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42602 39107 603 41 0 42561 0
vsize: 170408
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40619 0 0 0 45906 97 0 0 25 0 1 0 485535613 175173632 39269 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42767 39269 603 41 0 42726 0
vsize: 171068
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40719 0 0 0 46906 97 0 0 25 0 1 0 485535613 175595520 39369 4294967295 134512640 134672761 3221224528 3221223700 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 39369 603 41 0 42829 0
vsize: 171480
[startup+480.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40720 0 0 0 47906 97 0 0 25 0 1 0 485535613 175595520 39370 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 39370 603 41 0 42829 0
vsize: 171480
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40822 0 0 0 48906 97 0 0 25 0 1 0 485535613 176001024 39472 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42969 39472 603 41 0 42928 0
vsize: 171876
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 40946 0 0 0 49906 98 0 0 25 0 1 0 485535613 176537600 39596 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43100 39596 603 41 0 43059 0
vsize: 172400
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41064 0 0 0 50906 99 0 0 25 0 1 0 485535613 177078272 39714 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43232 39714 603 41 0 43191 0
vsize: 172928
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41168 0 0 0 51906 99 0 0 25 0 1 0 485535613 177475584 39818 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43329 39818 603 41 0 43288 0
vsize: 173316
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41263 0 0 0 52905 99 0 0 25 0 1 0 485535613 177876992 39913 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43427 39913 603 41 0 43386 0
vsize: 173708
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41395 0 0 0 53905 100 0 0 25 0 1 0 485535613 178393088 40045 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43553 40045 603 41 0 43512 0
vsize: 174212
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41525 0 0 0 54905 100 0 0 25 0 1 0 485535613 178941952 40175 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43687 40175 603 41 0 43646 0
vsize: 174748
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41645 0 0 0 55905 100 0 0 25 0 1 0 485535613 179347456 40295 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43786 40295 603 41 0 43745 0
vsize: 175144
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41741 0 0 0 56905 100 0 0 25 0 1 0 485535613 179884032 40391 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43917 40391 603 41 0 43876 0
vsize: 175668
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41846 0 0 0 57905 101 0 0 25 0 1 0 485535613 180285440 40496 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44015 40496 603 41 0 43974 0
vsize: 176060
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 41986 0 0 0 58905 101 0 0 25 0 1 0 485535613 180953088 40636 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44178 40636 603 41 0 44137 0
vsize: 176712
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 42158 0 0 0 59905 101 0 0 25 0 1 0 485535613 181612544 40808 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44339 40808 603 41 0 44298 0
vsize: 177356
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 42348 0 0 0 60905 101 0 0 25 0 1 0 485535613 182411264 40998 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44534 40998 603 41 0 44493 0
vsize: 178136
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 42563 0 0 0 61905 102 0 0 25 0 1 0 485535613 183218176 41213 4294967295 134512640 134672761 3221224528 3221223632 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44731 41213 603 41 0 44690 0
vsize: 178924
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 42785 0 0 0 62905 102 0 0 25 0 1 0 485535613 184152064 41435 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44959 41435 603 41 0 44918 0
vsize: 179836
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 42991 0 0 0 63905 103 0 0 25 0 1 0 485535613 185081856 41641 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45186 41641 603 41 0 45145 0
vsize: 180744
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 43184 0 0 0 64905 103 0 0 25 0 1 0 485535613 185745408 41834 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45348 41834 603 41 0 45307 0
vsize: 181392
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 43380 0 0 0 65904 104 0 0 25 0 1 0 485535613 186662912 42030 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45572 42030 603 41 0 45531 0
vsize: 182288
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 43576 0 0 0 66903 105 0 0 25 0 1 0 485535613 187461632 42226 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45767 42226 603 41 0 45726 0
vsize: 183068
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 43733 0 0 0 67903 105 0 0 25 0 1 0 485535613 188002304 42383 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45899 42383 603 41 0 45858 0
vsize: 183596
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 4881
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 43932 0 0 0 68903 105 0 0 25 0 1 0 485535613 188801024 42582 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46094 42582 603 41 0 46053 0
vsize: 184376
[startup+700.03 s]
Raw data (loadavg): 1.07 0.99 0.94 2/56 4928
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44115 0 0 0 69903 106 0 0 25 0 1 0 485535613 189591552 42765 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46287 42765 603 41 0 46246 0
vsize: 185148
[startup+710.03 s]
Raw data (loadavg): 1.21 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44280 0 0 0 70902 106 0 0 25 0 1 0 485535613 190251008 42930 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46448 42930 603 41 0 46407 0
vsize: 185792
[startup+720.03 s]
Raw data (loadavg): 1.18 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44453 0 0 0 71902 107 0 0 25 0 1 0 485535613 191053824 43103 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46644 43103 603 41 0 46603 0
vsize: 186576
[startup+730.03 s]
Raw data (loadavg): 1.15 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44638 0 0 0 72902 107 0 0 25 0 1 0 485535613 191713280 43288 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46805 43288 603 41 0 46764 0
vsize: 187220
[startup+740.031 s]
Raw data (loadavg): 1.13 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44807 0 0 0 73901 108 0 0 25 0 1 0 485535613 192380928 43457 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46968 43457 603 41 0 46927 0
vsize: 187872
[startup+750.031 s]
Raw data (loadavg): 1.11 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 44944 0 0 0 74901 109 0 0 25 0 1 0 485535613 193048576 43594 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47131 43594 603 41 0 47090 0
vsize: 188524
[startup+760.032 s]
Raw data (loadavg): 1.09 1.02 0.95 2/54 4934
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45098 0 0 0 75901 109 0 0 25 0 1 0 485535613 193585152 43748 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47262 43748 603 41 0 47221 0
vsize: 189048
[startup+770.032 s]
Raw data (loadavg): 1.08 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45280 0 0 0 76901 109 0 0 25 0 1 0 485535613 194387968 43930 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47458 43932 603 41 0 47417 0
vsize: 189832
[startup+780.032 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45445 0 0 0 77900 110 0 0 25 0 1 0 485535613 195039232 44095 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47617 44095 603 41 0 47576 0
vsize: 190468
[startup+790.032 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45596 0 0 0 78900 110 0 0 25 0 1 0 485535613 195702784 44246 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47779 44246 603 41 0 47738 0
vsize: 191116
[startup+800.033 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45755 0 0 0 79900 110 0 0 25 0 1 0 485535613 196243456 44405 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47911 44405 603 41 0 47870 0
vsize: 191644
[startup+810.032 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 45884 0 0 0 80900 110 0 0 25 0 1 0 485535613 196780032 44534 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48042 44534 603 41 0 48001 0
vsize: 192168
[startup+820.032 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46007 0 0 0 81900 111 0 0 25 0 1 0 485535613 197316608 44657 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48173 44657 603 41 0 48132 0
vsize: 192692
[startup+830.033 s]
Raw data (loadavg): 1.03 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46032 0 0 0 82900 111 0 0 25 0 1 0 485535613 197447680 44682 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48205 44682 603 41 0 48164 0
vsize: 192820
[startup+840.033 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46033 0 0 0 83900 111 0 0 25 0 1 0 485535613 197447680 44683 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48205 44683 603 41 0 48164 0
vsize: 192820
[startup+850.034 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46135 0 0 0 84901 111 0 0 25 0 1 0 485535613 197849088 44785 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48303 44785 603 41 0 48262 0
vsize: 193212
[startup+860.034 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46251 0 0 0 85901 111 0 0 25 0 1 0 485535613 198381568 44901 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48433 44901 603 41 0 48392 0
vsize: 193732
[startup+870.034 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46350 0 0 0 86901 111 0 0 25 0 1 0 485535613 198819840 45000 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48540 45000 603 41 0 48499 0
vsize: 194160
[startup+880.034 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46360 0 0 0 87899 111 0 0 25 0 1 0 485535613 198819840 45010 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48540 45010 603 41 0 48499 0
vsize: 194160
[startup+890.033 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46463 0 0 0 88899 112 0 0 25 0 1 0 485535613 199344128 45113 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45113 603 41 0 48627 0
vsize: 194672
[startup+900.035 s]
Raw data (loadavg): 1.01 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46464 0 0 0 89900 112 0 0 25 0 1 0 485535613 199344128 45114 4294967295 134512640 134672761 3221224528 3221223728 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45114 603 41 0 48627 0
vsize: 194672
[startup+910.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46464 0 0 0 90900 112 0 0 25 0 1 0 485535613 199344128 45114 4294967295 134512640 134672761 3221224528 3221223700 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45114 603 41 0 48627 0
vsize: 194672
[startup+920.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46483 0 0 0 91900 112 0 0 25 0 1 0 485535613 199344128 45133 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45133 603 41 0 48627 0
vsize: 194672
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46629 0 0 0 92900 112 0 0 25 0 1 0 485535613 200019968 45279 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48833 45279 603 41 0 48792 0
vsize: 195332
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46792 0 0 0 93900 112 0 0 25 0 1 0 485535613 200687616 45442 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48996 45442 603 41 0 48955 0
vsize: 195984
[startup+950.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 46978 0 0 0 94899 113 0 0 25 0 1 0 485535613 201482240 45628 4294967295 134512640 134672761 3221224528 3221223544 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49190 45629 603 41 0 49149 0
vsize: 196760
[startup+960.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 47189 0 0 0 95898 114 0 0 25 0 1 0 485535613 202285056 45839 4294967295 134512640 134672761 3221224528 3221223680 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49386 45839 603 41 0 49345 0
vsize: 197544
[startup+970.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 47368 0 0 0 96898 114 0 0 25 0 1 0 485535613 203079680 46018 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49580 46018 603 41 0 49539 0
vsize: 198320
[startup+980.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 47532 0 0 0 97898 115 0 0 25 0 1 0 485535613 203739136 46182 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49741 46182 603 41 0 49700 0
vsize: 198964
[startup+990.034 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 47701 0 0 0 98897 116 0 0 25 0 1 0 485535613 204406784 46351 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49904 46351 603 41 0 49863 0
vsize: 199616
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 47856 0 0 0 99897 116 0 0 25 0 1 0 485535613 205070336 46506 4294967295 134512640 134672761 3221224528 3221223664 134560598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50066 46506 603 41 0 50025 0
vsize: 200264
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 48041 0 0 0 100897 116 0 0 25 0 1 0 485535613 205729792 46691 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50227 46691 603 41 0 50186 0
vsize: 200908
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 48240 0 0 0 101896 117 0 0 25 0 1 0 485535613 206532608 46890 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50423 46890 603 41 0 50382 0
vsize: 201692
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 48479 0 0 0 102896 117 0 0 25 0 1 0 485535613 207597568 47129 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50683 47129 603 41 0 50642 0
vsize: 202732
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 48691 0 0 0 103896 118 0 0 25 0 1 0 485535613 208392192 47341 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50877 47341 603 41 0 50836 0
vsize: 203508
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 48903 0 0 0 104896 118 0 0 25 0 1 0 485535613 209313792 47553 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51102 47553 603 41 0 51061 0
vsize: 204408
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4936
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49142 0 0 0 105895 119 0 0 25 0 1 0 485535613 210247680 47792 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51330 47792 603 41 0 51289 0
vsize: 205320
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49344 0 0 0 106895 119 0 0 25 0 1 0 485535613 211046400 47994 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51525 47994 603 41 0 51484 0
vsize: 206100
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49462 0 0 0 107895 120 0 0 25 0 1 0 485535613 211587072 48112 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51657 48112 603 41 0 51616 0
vsize: 206628
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49574 0 0 0 108894 120 0 0 25 0 1 0 485535613 211992576 48224 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51756 48224 603 41 0 51715 0
vsize: 207024
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49692 0 0 0 109894 120 0 0 25 0 1 0 485535613 212533248 48342 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51888 48342 603 41 0 51847 0
vsize: 207552
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 49873 0 0 0 110894 121 0 0 25 0 1 0 485535613 213200896 48523 4294967295 134512640 134672761 3221224528 3221223632 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52051 48523 603 41 0 52010 0
vsize: 208204
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50010 0 0 0 111894 121 0 0 25 0 1 0 485535613 213876736 48660 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52216 48660 603 41 0 52175 0
vsize: 208864
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50151 0 0 0 112893 122 0 0 25 0 1 0 485535613 214409216 48801 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52346 48801 603 41 0 52305 0
vsize: 209384
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50326 0 0 0 113893 122 0 0 25 0 1 0 485535613 215072768 48976 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52508 48976 603 41 0 52467 0
vsize: 210032
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50462 0 0 0 114893 123 0 0 25 0 1 0 485535613 215728128 49112 4294967295 134512640 134672761 3221224528 3221223664 134560613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52668 49112 603 41 0 52627 0
vsize: 210672
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50558 0 0 0 115893 123 0 0 25 0 1 0 485535613 215994368 49208 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52733 49208 603 41 0 52692 0
vsize: 210932
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50656 0 0 0 116893 123 0 0 25 0 1 0 485535613 216399872 49306 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52832 49306 603 41 0 52791 0
vsize: 211328
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50745 0 0 0 117893 123 0 0 25 0 1 0 485535613 216805376 49395 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52931 49395 603 41 0 52890 0
vsize: 211724
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50830 0 0 0 118893 124 0 0 25 0 1 0 485535613 217202688 49480 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53028 49480 603 41 0 52987 0
vsize: 212112
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.95 2/54 4938
Raw data (stat): 4881 (minisat+) R 4880 5897 5896 0 -1 0 50966 0 0 0 119893 124 0 0 25 0 1 0 485535613 217731072 49616 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53157 49616 603 41 0 53116 0
vsize: 212628
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.95 1/54 4938
Raw data (stat): 4881 (minisat+) Z 4880 5897 5896 0 -1 12 50969 0 0 0 119893 133 0 0 25 0 1 0 485535613 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.14
CPU time (s): 1200.27
CPU user time (s): 1198.93
CPU system time (s): 1.3378
CPU usage (%): 100.011
Max. virtual memory (Kb): 212628
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####