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-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	920
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.75
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 15518

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        243008 kB
Buffers:         38484 kB
Cached:         712100 kB
SwapCached:          0 kB
Active:         267976 kB
Inactive:       485552 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        242756 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32440 kB
Committed_AS:    63712 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 05:04:31 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 17380 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.84 0.94 0.90 2/54 23718
Raw data (stat): 23718 (runsolver) R 23717 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542301976 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.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 34795 0 0 0 918 80 0 0 25 0 1 0 542301976 152027136 33466 4294967295 134512640 134672761 3221224528 3221215800 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37116 33466 603 41 0 37075 0
vsize: 148464
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35323 0 0 0 1916 81 0 0 25 0 1 0 542301976 152838144 33994 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37314 33994 603 41 0 37273 0
vsize: 149256
[startup+30.0005 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35405 0 0 0 2915 82 0 0 25 0 1 0 542301976 153112576 34076 4294967295 134512640 134672761 3221224528 3221223676 134560552 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.0004 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35433 0 0 0 3915 82 0 0 25 0 1 0 542301976 153251840 34104 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.0011 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35467 0 0 0 4915 82 0 0 25 0 1 0 542301976 153387008 34138 4294967295 134512640 134672761 3221224528 3221223692 134561235 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.0005 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35552 0 0 0 5915 82 0 0 25 0 1 0 542301976 153788416 34223 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37546 34223 603 41 0 37505 0
vsize: 150184
[startup+70.0005 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35619 0 0 0 6915 82 0 0 25 0 1 0 542301976 154058752 34290 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.0012 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35653 0 0 0 7915 82 0 0 25 0 1 0 542301976 154189824 34324 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37644 34324 603 41 0 37603 0
vsize: 150576
[startup+90.0005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35795 0 0 0 8914 83 0 0 25 0 1 0 542301976 154726400 34466 4294967295 134512640 134672761 3221224528 3221223700 134556634 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.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35895 0 0 0 9914 83 0 0 25 0 1 0 542301976 155127808 34566 4294967295 134512640 134672761 3221224528 3221223664 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37873 34566 603 41 0 37832 0
vsize: 151492
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 35960 0 0 0 10914 84 0 0 25 0 1 0 542301976 155398144 34631 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37939 34631 603 41 0 37898 0
vsize: 151756
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36117 0 0 0 11914 84 0 0 25 0 1 0 542301976 156073984 34788 4294967295 134512640 134672761 3221224528 3221223632 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38104 34788 603 41 0 38063 0
vsize: 152416
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36163 0 0 0 12914 84 0 0 25 0 1 0 542301976 156205056 34834 4294967295 134512640 134672761 3221224528 3221223700 134556598 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.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36164 0 0 0 13914 84 0 0 25 0 1 0 542301976 156205056 34835 4294967295 134512640 134672761 3221224528 3221223728 134557828 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.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36225 0 0 0 14914 84 0 0 25 0 1 0 542301976 156475392 34896 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38202 34896 603 41 0 38161 0
vsize: 152808
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36358 0 0 0 15914 85 0 0 25 0 1 0 542301976 157016064 35029 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38334 35029 603 41 0 38293 0
vsize: 153336
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 36968 0 0 0 16913 86 0 0 25 0 1 0 542301976 160235520 35618 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39120 35618 603 41 0 39079 0
vsize: 156480
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37029 0 0 0 17913 86 0 0 25 0 1 0 542301976 160501760 35679 4294967295 134512640 134672761 3221224528 3221223696 134560869 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.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37135 0 0 0 18912 87 0 0 25 0 1 0 542301976 160923648 35785 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39288 35785 603 41 0 39247 0
vsize: 157152
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37212 0 0 0 19912 87 0 0 25 0 1 0 542301976 161329152 35862 4294967295 134512640 134672761 3221224528 3221223664 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39387 35862 603 41 0 39346 0
vsize: 157548
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37308 0 0 0 20912 87 0 0 25 0 1 0 542301976 161599488 35958 4294967295 134512640 134672761 3221224528 3221223700 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39453 35958 603 41 0 39412 0
vsize: 157812
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37313 0 0 0 21911 87 0 0 25 0 1 0 542301976 161730560 35963 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39485 35963 603 41 0 39444 0
vsize: 157940
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37324 0 0 0 22911 87 0 0 25 0 1 0 542301976 161730560 35974 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39485 35974 603 41 0 39444 0
vsize: 157940
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37356 0 0 0 23911 87 0 0 25 0 1 0 542301976 161865728 36006 4294967295 134512640 134672761 3221224528 3221223728 134557895 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.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37424 0 0 0 24911 88 0 0 25 0 1 0 542301976 162131968 36074 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39583 36074 603 41 0 39542 0
vsize: 158332
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37589 0 0 0 25911 88 0 0 25 0 1 0 542301976 162807808 36239 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39748 36239 603 41 0 39707 0
vsize: 158992
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37739 0 0 0 26911 89 0 0 25 0 1 0 542301976 163340288 36389 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39878 36389 603 41 0 39837 0
vsize: 159512
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37882 0 0 0 27911 89 0 0 25 0 1 0 542301976 164012032 36532 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40042 36532 603 41 0 40001 0
vsize: 160168
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 37982 0 0 0 28911 89 0 0 25 0 1 0 542301976 164417536 36632 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40141 36632 603 41 0 40100 0
vsize: 160564
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38100 0 0 0 29911 89 0 0 25 0 1 0 542301976 164818944 36750 4294967295 134512640 134672761 3221224528 3221223664 134565078 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40239 36750 603 41 0 40198 0
vsize: 160956
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38275 0 0 0 30911 89 0 0 25 0 1 0 542301976 165621760 36925 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40435 36925 603 41 0 40394 0
vsize: 161740
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38422 0 0 0 31911 90 0 0 25 0 1 0 542301976 166309888 37072 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40603 37072 603 41 0 40562 0
vsize: 162412
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38535 0 0 0 32911 90 0 0 25 0 1 0 542301976 166715392 37185 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40702 37185 603 41 0 40661 0
vsize: 162808
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38660 0 0 0 33910 90 0 0 25 0 1 0 542301976 167251968 37310 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40833 37310 603 41 0 40792 0
vsize: 163332
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38802 0 0 0 34911 90 0 0 25 0 1 0 542301976 167776256 37452 4294967295 134512640 134672761 3221224528 3221223632 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40961 37452 603 41 0 40920 0
vsize: 163844
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 38888 0 0 0 35911 91 0 0 25 0 1 0 542301976 168181760 37538 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41060 37538 603 41 0 41019 0
vsize: 164240
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39007 0 0 0 36911 91 0 0 25 0 1 0 542301976 168587264 37657 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41159 37657 603 41 0 41118 0
vsize: 164636
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39183 0 0 0 37910 91 0 0 25 0 1 0 542301976 169394176 37833 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41356 37833 603 41 0 41315 0
vsize: 165424
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39343 0 0 0 38910 92 0 0 25 0 1 0 542301976 170061824 37993 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41519 37993 603 41 0 41478 0
vsize: 166076
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39507 0 0 0 39910 92 0 0 25 0 1 0 542301976 170737664 38157 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41684 38157 603 41 0 41643 0
vsize: 166736
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39689 0 0 0 40909 93 0 0 25 0 1 0 542301976 171413504 38339 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41849 38339 603 41 0 41808 0
vsize: 167396
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 39880 0 0 0 41909 93 0 0 25 0 1 0 542301976 172216320 38530 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42045 38530 603 41 0 42004 0
vsize: 168180
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40056 0 0 0 42909 94 0 0 25 0 1 0 542301976 172888064 38706 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42209 38706 603 41 0 42168 0
vsize: 168836
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40252 0 0 0 43908 94 0 0 25 0 1 0 542301976 173699072 38902 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42407 38902 603 41 0 42366 0
vsize: 169628
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40434 0 0 0 44908 95 0 0 25 0 1 0 542301976 174497792 39084 4294967295 134512640 134672761 3221224528 3221223664 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42602 39084 603 41 0 42561 0
vsize: 170408
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40605 0 0 0 45908 95 0 0 25 0 1 0 542301976 175173632 39255 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42767 39255 603 41 0 42726 0
vsize: 171068
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40719 0 0 0 46908 96 0 0 25 0 1 0 542301976 175595520 39369 4294967295 134512640 134672761 3221224528 3221223700 134556688 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.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40719 0 0 0 47908 96 0 0 25 0 1 0 542301976 175595520 39369 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42870 39369 603 41 0 42829 0
vsize: 171480
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40800 0 0 0 48908 96 0 0 25 0 1 0 542301976 176001024 39450 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42969 39450 603 41 0 42928 0
vsize: 171876
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 40925 0 0 0 49908 96 0 0 25 0 1 0 542301976 176402432 39575 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43067 39575 603 41 0 43026 0
vsize: 172268
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41044 0 0 0 50908 96 0 0 25 0 1 0 542301976 176943104 39694 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43199 39694 603 41 0 43158 0
vsize: 172796
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41150 0 0 0 51908 97 0 0 25 0 1 0 542301976 177344512 39800 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43297 39800 603 41 0 43256 0
vsize: 173188
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41244 0 0 0 52907 97 0 0 25 0 1 0 542301976 177741824 39894 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43394 39894 603 41 0 43353 0
vsize: 173576
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41362 0 0 0 53907 97 0 0 25 0 1 0 542301976 178274304 40012 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43524 40012 603 41 0 43483 0
vsize: 174096
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41508 0 0 0 54907 98 0 0 25 0 1 0 542301976 178806784 40158 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43654 40158 603 41 0 43613 0
vsize: 174616
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41622 0 0 0 55907 98 0 0 25 0 1 0 542301976 179347456 40272 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43786 40272 603 41 0 43745 0
vsize: 175144
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41707 0 0 0 56907 98 0 0 25 0 1 0 542301976 179621888 40357 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43853 40357 603 41 0 43812 0
vsize: 175412
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41824 0 0 0 57908 98 0 0 25 0 1 0 542301976 180285440 40474 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44015 40474 603 41 0 43974 0
vsize: 176060
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 41954 0 0 0 58907 98 0 0 25 0 1 0 542301976 180817920 40604 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44145 40604 603 41 0 44104 0
vsize: 176580
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 42119 0 0 0 59907 99 0 0 25 0 1 0 542301976 181481472 40769 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44307 40769 603 41 0 44266 0
vsize: 177228
[startup+610.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 42309 0 0 0 60907 99 0 0 25 0 1 0 542301976 182280192 40959 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44502 40959 603 41 0 44461 0
vsize: 178008
[startup+620.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 42513 0 0 0 61907 99 0 0 25 0 1 0 542301976 183083008 41163 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44698 41163 603 41 0 44657 0
vsize: 178792
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 42732 0 0 0 62906 100 0 0 25 0 1 0 542301976 184016896 41382 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44926 41382 603 41 0 44885 0
vsize: 179704
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 42950 0 0 0 63906 101 0 0 25 0 1 0 542301976 184815616 41600 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45121 41600 603 41 0 45080 0
vsize: 180484
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 43125 0 0 0 64906 101 0 0 25 0 1 0 542301976 185610240 41775 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45315 41775 603 41 0 45274 0
vsize: 181260
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 43335 0 0 0 65905 102 0 0 25 0 1 0 542301976 186396672 41985 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45507 41985 603 41 0 45466 0
vsize: 182028
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 43521 0 0 0 66905 102 0 0 25 0 1 0 542301976 187199488 42171 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45703 42171 603 41 0 45662 0
vsize: 182812
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 43686 0 0 0 67905 102 0 0 25 0 1 0 542301976 187867136 42336 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45866 42336 603 41 0 45825 0
vsize: 183464
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 43882 0 0 0 68905 103 0 0 25 0 1 0 542301976 188665856 42532 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46061 42532 603 41 0 46020 0
vsize: 184244
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44069 0 0 0 69904 103 0 0 25 0 1 0 542301976 189464576 42719 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46256 42719 603 41 0 46215 0
vsize: 185024
[startup+710.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44237 0 0 0 70904 104 0 0 25 0 1 0 542301976 190119936 42887 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46416 42887 603 41 0 46375 0
vsize: 185664
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44406 0 0 0 71904 105 0 0 25 0 1 0 542301976 190791680 43056 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46580 43056 603 41 0 46539 0
vsize: 186320
[startup+730.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44597 0 0 0 72903 105 0 0 25 0 1 0 542301976 191586304 43247 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46774 43247 603 41 0 46733 0
vsize: 187096
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44761 0 0 0 73903 106 0 0 25 0 1 0 542301976 192253952 43411 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46937 43411 603 41 0 46896 0
vsize: 187748
[startup+750.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 44903 0 0 0 74903 106 0 0 25 0 1 0 542301976 192778240 43553 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47065 43553 603 41 0 47024 0
vsize: 188260
[startup+760.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45054 0 0 0 75903 106 0 0 25 0 1 0 542301976 193454080 43704 4294967295 134512640 134672761 3221224528 3221223664 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47230 43704 603 41 0 47189 0
vsize: 188920
[startup+770.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45228 0 0 0 76902 107 0 0 25 0 1 0 542301976 194121728 43878 4294967295 134512640 134672761 3221224528 3221223632 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47393 43878 603 41 0 47352 0
vsize: 189572
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45378 0 0 0 77902 107 0 0 25 0 1 0 542301976 194777088 44028 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47553 44028 603 41 0 47512 0
vsize: 190212
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45544 0 0 0 78902 108 0 0 25 0 1 0 542301976 195432448 44194 4294967295 134512640 134672761 3221224528 3221223712 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47713 44194 603 41 0 47672 0
vsize: 190852
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45718 0 0 0 79902 108 0 0 25 0 1 0 542301976 196108288 44368 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47878 44368 603 41 0 47837 0
vsize: 191512
[startup+810.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45841 0 0 0 80902 108 0 0 25 0 1 0 542301976 196644864 44491 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48009 44491 603 41 0 47968 0
vsize: 192036
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 45988 0 0 0 81901 109 0 0 25 0 1 0 542301976 197316608 44638 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48173 44638 603 41 0 48132 0
vsize: 192692
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46032 0 0 0 82901 109 0 0 25 0 1 0 542301976 197447680 44682 4294967295 134512640 134672761 3221224528 3221223700 134556688 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46032 0 0 0 83901 109 0 0 25 0 1 0 542301976 197447680 44682 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48205 44682 603 41 0 48164 0
vsize: 192820
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46108 0 0 0 84901 109 0 0 25 0 1 0 542301976 197713920 44758 4294967295 134512640 134672761 3221224528 3221223692 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48270 44758 603 41 0 48229 0
vsize: 193080
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46218 0 0 0 85901 109 0 0 25 0 1 0 542301976 198250496 44868 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48401 44868 603 41 0 48360 0
vsize: 193604
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46347 0 0 0 86901 110 0 0 25 0 1 0 542301976 198819840 44997 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48540 44997 603 41 0 48499 0
vsize: 194160
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46358 0 0 0 87901 110 0 0 25 0 1 0 542301976 198819840 45008 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48540 45008 603 41 0 48499 0
vsize: 194160
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46463 0 0 0 88901 110 0 0 25 0 1 0 542301976 199344128 45113 4294967295 134512640 134672761 3221224528 3221223696 134561234 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46463 0 0 0 89901 110 0 0 25 0 1 0 542301976 199344128 45113 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45113 603 41 0 48627 0
vsize: 194672
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46464 0 0 0 90901 110 0 0 25 0 1 0 542301976 199344128 45114 4294967295 134512640 134672761 3221224528 3221223700 134556682 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46464 0 0 0 91901 110 0 0 25 0 1 0 542301976 199344128 45114 4294967295 134512640 134672761 3221224528 3221223700 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 45114 603 41 0 48627 0
vsize: 194672
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23718
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46579 0 0 0 92901 111 0 0 25 0 1 0 542301976 199749632 45229 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48767 45229 603 41 0 48726 0
vsize: 195068
[startup+940.014 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 23759
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46729 0 0 0 93901 111 0 0 25 0 1 0 542301976 200417280 45379 4294967295 134512640 134672761 3221224528 3221223632 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48930 45379 603 41 0 48889 0
vsize: 195720
[startup+950.013 s]
Raw data (loadavg): 1.22 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 46914 0 0 0 94901 111 0 0 25 0 1 0 542301976 201220096 45564 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49126 45564 603 41 0 49085 0
vsize: 196504
[startup+960.013 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47109 0 0 0 95900 112 0 0 25 0 1 0 542301976 202018816 45759 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49321 45759 603 41 0 49280 0
vsize: 197284
[startup+970.013 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47310 0 0 0 96900 112 0 0 25 0 1 0 542301976 202817536 45960 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49516 45960 603 41 0 49475 0
vsize: 198064
[startup+980.013 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47475 0 0 0 97899 113 0 0 25 0 1 0 542301976 203476992 46125 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49677 46125 603 41 0 49636 0
vsize: 198708
[startup+990.013 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47654 0 0 0 98899 113 0 0 25 0 1 0 542301976 204140544 46304 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49839 46304 603 41 0 49798 0
vsize: 199356
[startup+1000.01 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 23771
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47797 0 0 0 99899 114 0 0 25 0 1 0 542301976 204812288 46447 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50003 46447 603 41 0 49962 0
vsize: 200012
[startup+1010.01 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 47974 0 0 0 100899 114 0 0 25 0 1 0 542301976 205467648 46624 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50163 46624 603 41 0 50122 0
vsize: 200652
[startup+1020.01 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 48160 0 0 0 101898 115 0 0 25 0 1 0 542301976 206266368 46810 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50358 46810 603 41 0 50317 0
vsize: 201432
[startup+1030.01 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 48375 0 0 0 102898 115 0 0 25 0 1 0 542301976 207204352 47025 4294967295 134512640 134672761 3221224528 3221223696 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50587 47025 603 41 0 50546 0
vsize: 202348
[startup+1040.01 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 48606 0 0 0 103898 115 0 0 25 0 1 0 542301976 208121856 47256 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50811 47256 603 41 0 50770 0
vsize: 203244
[startup+1050.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 48825 0 0 0 104898 116 0 0 25 0 1 0 542301976 208916480 47475 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51005 47475 603 41 0 50964 0
vsize: 204020
[startup+1060.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49031 0 0 0 105898 116 0 0 25 0 1 0 542301976 209842176 47681 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51231 47681 603 41 0 51190 0
vsize: 204924
[startup+1070.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49261 0 0 0 106896 118 0 0 25 0 1 0 542301976 210776064 47911 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51459 47911 603 41 0 51418 0
vsize: 205836
[startup+1080.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49411 0 0 0 107896 118 0 0 25 0 1 0 542301976 211316736 48061 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51591 48061 603 41 0 51550 0
vsize: 206364
[startup+1090.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49530 0 0 0 108896 118 0 0 25 0 1 0 542301976 211857408 48180 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51723 48180 603 41 0 51682 0
vsize: 206892
[startup+1100.01 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49645 0 0 0 109896 118 0 0 25 0 1 0 542301976 212262912 48295 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51822 48295 603 41 0 51781 0
vsize: 207288
[startup+1110.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49791 0 0 0 110896 119 0 0 25 0 1 0 542301976 212938752 48441 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51987 48441 603 41 0 51946 0
vsize: 207948
[startup+1120.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 49951 0 0 0 111895 120 0 0 25 0 1 0 542301976 213606400 48601 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52150 48601 603 41 0 52109 0
vsize: 208600
[startup+1130.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50084 0 0 0 112895 120 0 0 25 0 1 0 542301976 214142976 48734 4294967295 134512640 134672761 3221224528 3221223664 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52281 48734 603 41 0 52240 0
vsize: 209124
[startup+1140.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50245 0 0 0 113895 121 0 0 25 0 1 0 542301976 214802432 48895 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52442 48895 603 41 0 52401 0
vsize: 209768
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50400 0 0 0 114894 121 0 0 25 0 1 0 542301976 215461888 49050 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52603 49050 603 41 0 52562 0
vsize: 210412
[startup+1160.01 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50516 0 0 0 115894 121 0 0 25 0 1 0 542301976 215863296 49166 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52701 49166 603 41 0 52660 0
vsize: 210804
[startup+1170.01 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50614 0 0 0 116894 122 0 0 25 0 1 0 542301976 216264704 49264 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52799 49264 603 41 0 52758 0
vsize: 211196
[startup+1180.02 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50706 0 0 0 117894 122 0 0 25 0 1 0 542301976 216670208 49356 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52898 49356 603 41 0 52857 0
vsize: 211592
[startup+1190.01 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50794 0 0 0 118894 122 0 0 25 0 1 0 542301976 217067520 49444 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52995 49444 603 41 0 52954 0
vsize: 211980
[startup+1200.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 23773
Raw data (stat): 23718 (minisat+) R 23717 22612 22611 0 -1 0 50889 0 0 0 119894 122 0 0 25 0 1 0 542301976 217473024 49539 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53094 49539 603 41 0 53053 0
vsize: 212376
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 1.04 1.01 0.93 1/54 23773
Raw data (stat): 23718 (minisat+) Z 23717 22612 22611 0 -1 12 50892 0 0 0 119895 132 0 0 25 0 1 0 542301976 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.12
CPU time (s): 1200.27
CPU user time (s): 1198.95
CPU system time (s): 1.3228
CPU usage (%): 100.013
Max. virtual memory (Kb): 212376
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####