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/submitted/een/normalized-seymour.opb
MD5SUM	23a177449585151350479e80b33e6416
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	353
Optimality of the best value was proved	NO
Number of terms in the objective function	1372
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1372
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1372
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04984
Number of variables	1255
Total number of constraints	4827
Number of constraints which are clauses	4827
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	19
Trace number 6922

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 20:26:27 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4997 boxname=wulflinc2 idbench=385 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  23a177449585151350479e80b33e6416  /oldhome/oroussel/tmp/wulflinc2/normalized-seymour.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-seymour.opb
IDLAUNCH: 4997
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        880008 kB
Buffers:         36020 kB
Cached:          97528 kB
SwapCached:          4 kB
Active:          62156 kB
Inactive:        74224 kB
HighTotal:      131008 kB
HighFree:        29652 kB
LowTotal:       903652 kB
LowFree:        850356 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12720 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 20:46:29 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 4997 7 1200.09 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4827 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4827    33432 |    1609       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 349[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:76410     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   98923   253123 |   32974       0        0     nan |  0.000 % |
c |       100 |   97075   249222 |   36271      53      306     5.8 |  1.611 % |
c |       250 |   96306   247533 |   39898     182     1434     7.9 |  2.335 % |
c |       475 |   94983   244630 |   43888     352     2733     7.8 |  3.580 % |
c |       813 |   93755   241908 |   48277     659     6082     9.2 |  4.756 % |
c |      1319 |   92568   239259 |   53104    1107    10103     9.1 |  5.908 % |
c |      2079 |   91909   237778 |   58415    1848    16788     9.1 |  6.556 % |
c |      3218 |   91411   236662 |   64256    2962    28061     9.5 |  7.042 % |
c |      4926 |   90331   234236 |   70682    4606    53966    11.7 |  8.078 % |
c |      7488 |   90120   233759 |   77750    7151    98759    13.8 |  8.279 % |
c |     11332 |   89899   233266 |   85526   10979   176068    16.0 |  8.478 % |
c |     17098 |   89285   231884 |   94078   16657   308712    18.5 |  9.049 % |
c |     25749 |   89112   231493 |  103486   25255   976019    38.6 |  9.212 % |
c |     38723 |   89001   231242 |  113835   38209  1772808    46.4 |  9.316 % |
c |     58184 |   88950   231133 |  125218   57664  4775966    82.8 |  9.357 % |
c |     87378 |   88942   231115 |  137740   86849  9904394   114.0 |  9.365 % |
c |    131169 |   88746   230668 |  151514  130531 13442173   103.0 |  9.548 % |
c |    196853 |   88719   230611 |  166666   44042  6107081   138.7 |  9.572 % |
c |    295379 |   88664   230490 |  183332  142564 10444974    73.3 |  9.624 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -x0 x1 -x2 -x3 x4 -x5 -x6 -x7 x8 -x9 x10 -x11 x12 -x13 -x14 x15 -x16 -x17 x18 -x19 -x20 -x21 -x22 x23 -x24 x25 x26 x27 -x28 -x29 -x30 -x31 -x32 x33 x34 -x35 -x36 x37 -x38 -x39 -x40 x41 x42 -x43 x44 x45 x46 -x47 -x48 x49 -x50 -x51 x52 x53 x54 -x55 x56 x57 x58 -x59 -x60 x61 x62 x63 -x64 x65 x66 x67 x68 x69 -x70 -x71 -x72 -x73 -x74 x75 -x76 -x77 -x78 -x79 x80 x81 x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 x90 x91 -x92 -x93 x94 x95 -x96 -x97 -x98 x99 x100 -x101 -x102 -x103 -x104 -x105 x106 -x107 x108 -x109 x110 x111 x112 -x113 -x114 -x115 x116 -x117 -x118 -x119 -x120 -x121 -x122 x123 -x124 -x125 x126 -x127 x128 -x129 -x130 x131 -x132 -x133 -x134 x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 x143 -x144 -x145 -x146 -x147 x148 x149 -x150 -x151 x152 x153 -x154 -x155 -x156 -x157 x158 -x159 x160 -x161 -x162 -x163 -x164 x165 -x166 -x167 -x168 x169 x170 -x171 -x172 x173 -x174 -x175 -x176 -x177 -x178 x179 -x180 -x181 -x182 -x183 x184 x185 x186 -x187 -x188 x189 -x190 -x191 x192 x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 x204 -x205 -x206 -x207 -x208 -x209 -x210 x211 x212 -x213 -x214 -x215 x216 -x217 x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 x227 x228 -x229 -x230 x231 x232 -x233 x234 x235 -x236 -x237 x238 -x239 -x240 -x241 x242 -x243 x244 -x245 x246 -x247 -x248 x249 -x250 -x251 x252 -x253 x254 -x255 -x256 -x257 -x258 -x259 x260 -x261 -x262 x263 -x264 -x265 x266 -x267 x268 -x269 -x270 x271 -x272 x273 -x274 -x275 x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 x284 -x285 x286 x287 -x288 -x289 -x290 x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 x308 -x309 -x310 -x311 -x312 x313 x314 -x315 -x316 -x317 -x318 x319 -x320 x321 -x322 -x323 -x324 x325 -x326 -x327 x328 -x329 -x330 -x331 x332 -x333 x334 x335 -x336 -x337 x338 x339 x340 -x341 -x342 x343 x344 -x345 x346 -x347 -x348 -x349 -x350 -x351 -x352 x353 -x354 -x355 -x356 -x357 -x358 -x359 -x360 -x361 -x362 -x363 -x364 x365 -x366 x367 x368 -x369 -x370 -x371 -x372 -x373 x374 -x375 -x376 -x377 x378 -x379 -x380 x381 -x382 -x383 -x384 -x385 -x386 -x387 -x388 -x389 x390 x391 x392 -x393 -x394 -x395 x396 -x397 -x398 -x399 -x400 -x401 -x402 -x403 x404 -x405 -x406 -x407 -x408 -x409 -x410 -x411 -x412 -x413 -x414 x415 -x416 -x417 -x418 -x419 -x420 -x421 -x422 x423 x424 x425 x426 -x427 x428 x429 x430 x431 x432 -x433 -x434 -x435 x436 x437 x438 -x439 -x440 x441 -x442 x443 -x444 x445 x446 -x447 -x448 -x449 -x450 -x451 -x452 x453 x454 x455 x456 -x457 x458 -x459 x460 x461 x462 x463 x464 x465 -x466 x467 -x468 x469 -x470 x471 -x472 -x473 -x474 x475 x476 x477 x478 x479 x480 -x481 -x482 x483 -x484 x485 x486 -x487 -x488 x489 x490 x491 -x492 x493 -x494 -x495 -x496 -x497 x498 -x499 x500 x501 -x502 -x503 x504 x505 -x506 -x507 -x508 -x509 x510 x511 -x512 x513 -x514 x515 -x516 x517 -x518 x519 x520 -x521 -x522 x523 -x524 -x525 -x526 x527 x528 -x529 -x530 -x531 -x532 -x533 x534 -x535 -x536 -x537 x538 -x539 -x540 -x541 -x542 -x543 -x544 x545 -x546 x547 x548 -x549 -x550 -x551 x552 x553 x554 -x555 -x556 -x557 -x558 x559 -x560 -x561 x562 -x563 x564 x565 x566 x567 -x568 -x569 x570 -x571 -x572 -x573 x574 -x575 x576 x577 x578 -x579 -x580 x581 -x582 x583 -x584 -x585 -x586 x587 -x588 x589 -x590 -x591 -x592 -x593 x594 -x595 -x596 x597 -x598 -x599 -x600 x601 x602 x603 -x604 -x605 -x606 -x607 -x608 x609 x610 x611 x612 -x613 -x614 -x615 x616 -x617 -x618 -x619 -x620 -x621 -x622 x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 x632 -x633 x634 -x635 -x636 -x637 x638 x639 x640 x641 -x642 -x643 -x644 x645 x646 x647 -x648 x649 -x650 x651 -x652 -x653 -x654 -x655 x656 -x657 -x658 -x659 -x660 -x661 x662 -x663 x664 x665 x666 x667 -x668 x669 -x670 x671 x672 -x673 -x674 -x675 -x676 x677 x678 -x679 -x680 x681 -x682 x683 -x684 x685 -x686 -x687 x688 -x689 -x690 -x691 -x692 -x693 -x694 -x695 -x696 x697 -x698 -x699 -x700 -x701 -x702 -x703 -x704 x705 -x706 -x707 -x708 x709 -x710 -x711 -x712 -x713 -x714 -x715 -x716 -x717 x718 x719 -x720 -x721 -x722 x723 -x724 -x725 x726 -x727 x728 x729 -x730 -x731 -x732 -x733 -x734 -x735 -x736 -x7#### 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.41 0.13 0.04 2/54 32409
Raw data (stat): 32409 (runsolver) R 32408 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429241814 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.50 0.16 0.05 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 5051 0 0 0 985 13 0 0 25 0 1 0 429241814 23023616 4889 4294967295 134512640 134672761 3221224640 3221223812 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5621 4889 603 41 0 5580 0
vsize: 22484
[startup+20.0014 s]
Raw data (loadavg): 0.58 0.19 0.06 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 5216 0 0 0 1985 14 0 0 25 0 1 0 429241814 23699456 5054 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5786 5054 603 41 0 5745 0
vsize: 23144
[startup+30.0016 s]
Raw data (loadavg): 0.64 0.21 0.07 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 5446 0 0 0 2984 15 0 0 25 0 1 0 429241814 24649728 5284 4294967295 134512640 134672761 3221224640 3221223764 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6018 5284 603 41 0 5977 0
vsize: 24072
[startup+40.0018 s]
Raw data (loadavg): 0.70 0.24 0.08 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 5656 0 0 0 3983 15 0 0 25 0 1 0 429241814 25477120 5494 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6220 5494 603 41 0 6179 0
vsize: 24880
[startup+50.0025 s]
Raw data (loadavg): 0.74 0.26 0.09 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 6006 0 0 0 4981 17 0 0 25 0 1 0 429241814 26943488 5844 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6578 5844 603 41 0 6537 0
vsize: 26312
[startup+60.0027 s]
Raw data (loadavg): 0.78 0.29 0.10 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 6258 0 0 0 5979 19 0 0 25 0 1 0 429241814 28012544 6096 4294967295 134512640 134672761 3221224640 3221223808 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6839 6096 603 41 0 6798 0
vsize: 27356
[startup+70.0028 s]
Raw data (loadavg): 0.81 0.31 0.11 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 6533 0 0 0 6978 20 0 0 25 0 1 0 429241814 29085696 6371 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7101 6371 603 41 0 7060 0
vsize: 28404
[startup+80.0036 s]
Raw data (loadavg): 0.84 0.33 0.12 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 6829 0 0 0 7977 21 0 0 25 0 1 0 429241814 30416896 6667 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7426 6667 603 41 0 7385 0
vsize: 29704
[startup+90.0037 s]
Raw data (loadavg): 0.87 0.35 0.13 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 7243 0 0 0 8975 23 0 0 25 0 1 0 429241814 32034816 7081 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7821 7081 603 41 0 7780 0
vsize: 31284
[startup+100.004 s]
Raw data (loadavg): 0.89 0.37 0.14 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 7591 0 0 0 9974 24 0 0 25 0 1 0 429241814 33509376 7429 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8181 7429 603 41 0 8140 0
vsize: 32724
[startup+110.005 s]
Raw data (loadavg): 0.90 0.39 0.14 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 7905 0 0 0 10973 25 0 0 25 0 1 0 429241814 34844672 7743 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8507 7743 603 41 0 8466 0
vsize: 34028
[startup+120.005 s]
Raw data (loadavg): 0.92 0.41 0.15 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 8265 0 0 0 11971 27 0 0 25 0 1 0 429241814 36188160 8103 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8835 8103 603 41 0 8794 0
vsize: 35340
[startup+130.006 s]
Raw data (loadavg): 0.93 0.43 0.16 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 8616 0 0 0 12970 28 0 0 25 0 1 0 429241814 37658624 8454 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9194 8454 603 41 0 9153 0
vsize: 36776
[startup+140.007 s]
Raw data (loadavg): 0.94 0.45 0.17 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 8998 0 0 0 13968 30 0 0 25 0 1 0 429241814 39276544 8836 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9589 8836 603 41 0 9548 0
vsize: 38356
[startup+150.007 s]
Raw data (loadavg): 0.95 0.47 0.18 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 9366 0 0 0 14966 31 0 0 25 0 1 0 429241814 40759296 9204 4294967295 134512640 134672761 3221224640 3221223744 134559955 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9951 9204 603 41 0 9910 0
vsize: 39804
[startup+160.007 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 9736 0 0 0 15965 32 0 0 25 0 1 0 429241814 42250240 9574 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10315 9574 603 41 0 10274 0
vsize: 41260
[startup+170.007 s]
Raw data (loadavg): 0.96 0.50 0.20 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 10093 0 0 0 16964 34 0 0 25 0 1 0 429241814 43737088 9931 4294967295 134512640 134672761 3221224640 3221223736 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10678 9931 603 41 0 10637 0
vsize: 42712
[startup+180.007 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 10461 0 0 0 17963 35 0 0 25 0 1 0 429241814 45207552 10299 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11037 10299 603 41 0 10996 0
vsize: 44148
[startup+190.008 s]
Raw data (loadavg): 0.97 0.53 0.21 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 10760 0 0 0 18961 36 0 0 25 0 1 0 429241814 46419968 10598 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11333 10598 603 41 0 11292 0
vsize: 45332
[startup+200.008 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 11411 0 0 0 19959 38 0 0 25 0 1 0 429241814 49246208 11249 4294967295 134512640 134672761 3221224640 3221223744 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12023 11249 603 41 0 11982 0
vsize: 48092
[startup+210.008 s]
Raw data (loadavg): 0.98 0.56 0.23 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 12013 0 0 0 20957 40 0 0 25 0 1 0 429241814 51822592 11851 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12652 11851 603 41 0 12611 0
vsize: 50608
[startup+220.008 s]
Raw data (loadavg): 0.98 0.58 0.23 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 12570 0 0 0 21956 41 0 0 25 0 1 0 429241814 53985280 12408 4294967295 134512640 134672761 3221224640 3221223824 134559542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13180 12408 603 41 0 13139 0
vsize: 52720
[startup+230.009 s]
Raw data (loadavg): 0.98 0.59 0.24 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 13134 0 0 0 22955 42 0 0 25 0 1 0 429241814 56410112 12972 4294967295 134512640 134672761 3221224640 3221223744 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13772 12972 603 41 0 13731 0
vsize: 55088
[startup+240.009 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 13707 0 0 0 23952 45 0 0 25 0 1 0 429241814 58699776 13545 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14331 13545 603 41 0 14290 0
vsize: 57324
[startup+250.009 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 14220 0 0 0 24950 47 0 0 25 0 1 0 429241814 60854272 14058 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14857 14058 603 41 0 14816 0
vsize: 59428
[startup+260.011 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 14720 0 0 0 25948 49 0 0 25 0 1 0 429241814 62877696 14558 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15351 14558 603 41 0 15310 0
vsize: 61404
[startup+270.01 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 15205 0 0 0 26947 50 0 0 25 0 1 0 429241814 64786432 15043 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15817 15043 603 41 0 15776 0
vsize: 63268
[startup+280.011 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 15634 0 0 0 27945 52 0 0 25 0 1 0 429241814 66539520 15472 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16245 15472 603 41 0 16204 0
vsize: 64980
[startup+290.012 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 15888 0 0 0 28944 53 0 0 25 0 1 0 429241814 67633152 15726 4294967295 134512640 134672761 3221224640 3221223808 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16512 15726 603 41 0 16471 0
vsize: 66048
[startup+300.011 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 16216 0 0 0 29943 54 0 0 25 0 1 0 429241814 68972544 16054 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16839 16054 603 41 0 16798 0
vsize: 67356
[startup+310.012 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 16592 0 0 0 30941 56 0 0 25 0 1 0 429241814 70447104 16430 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17199 16430 603 41 0 17158 0
vsize: 68796
[startup+320.011 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 16891 0 0 0 31940 57 0 0 25 0 1 0 429241814 71651328 16729 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17493 16729 603 41 0 17452 0
vsize: 69972
[startup+330.011 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 17081 0 0 0 32938 58 0 0 25 0 1 0 429241814 72450048 16919 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17688 16919 603 41 0 17647 0
vsize: 70752
[startup+340.012 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 17228 0 0 0 33938 59 0 0 25 0 1 0 429241814 73138176 17066 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17856 17066 603 41 0 17815 0
vsize: 71424
[startup+350.011 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 17422 0 0 0 34936 60 0 0 25 0 1 0 429241814 73809920 17260 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18020 17260 603 41 0 17979 0
vsize: 72080
[startup+360.012 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 17807 0 0 0 35934 62 0 0 25 0 1 0 429241814 75423744 17645 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18414 17645 603 41 0 18373 0
vsize: 73656
[startup+370.012 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 18238 0 0 0 36932 64 0 0 25 0 1 0 429241814 77156352 18076 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18837 18076 603 41 0 18796 0
vsize: 75348
[startup+380.012 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 18661 0 0 0 37931 65 0 0 25 0 1 0 429241814 78897152 18499 4294967295 134512640 134672761 3221224640 3221223792 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19262 18499 603 41 0 19221 0
vsize: 77048
[startup+390.013 s]
Raw data (loadavg): 0.99 0.75 0.36 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 18995 0 0 0 38929 67 0 0 25 0 1 0 429241814 80236544 18833 4294967295 134512640 134672761 3221224640 3221223776 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19589 18833 603 41 0 19548 0
vsize: 78356
[startup+400.013 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 19333 0 0 0 39928 68 0 0 25 0 1 0 429241814 81580032 19171 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19917 19171 603 41 0 19876 0
vsize: 79668
[startup+410.013 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 19682 0 0 0 40927 69 0 0 25 0 1 0 429241814 83042304 19520 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20274 19520 603 41 0 20233 0
vsize: 81096
[startup+420.013 s]
Raw data (loadavg): 0.99 0.78 0.37 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 19863 0 0 0 41926 70 0 0 25 0 1 0 429241814 84238336 19701 4294967295 134512640 134672761 3221224640 3221223744 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20566 19701 603 41 0 20525 0
vsize: 82264
[startup+430.014 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 20022 0 0 0 42924 71 0 0 25 0 1 0 429241814 84910080 19860 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20730 19860 603 41 0 20689 0
vsize: 82920
[startup+440.015 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 20337 0 0 0 43923 72 0 0 25 0 1 0 429241814 86257664 20175 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21059 20175 603 41 0 21018 0
vsize: 84236
[startup+450.014 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 20693 0 0 0 44921 74 0 0 25 0 1 0 429241814 87724032 20531 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21417 20531 603 41 0 21376 0
vsize: 85668
[startup+460.014 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 21087 0 0 0 45920 76 0 0 25 0 1 0 429241814 89206784 20925 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21779 20925 603 41 0 21738 0
vsize: 87116
[startup+470.014 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 21494 0 0 0 46919 77 0 0 25 0 1 0 429241814 90939392 21332 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22202 21332 603 41 0 22161 0
vsize: 88808
[startup+480.015 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 21852 0 0 0 47917 79 0 0 25 0 1 0 429241814 92413952 21690 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22562 21690 603 41 0 22521 0
vsize: 90248
[startup+490.015 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 22204 0 0 0 48915 80 0 0 25 0 1 0 429241814 93880320 22042 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22920 22042 603 41 0 22879 0
vsize: 91680
[startup+500.016 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 22554 0 0 0 49914 82 0 0 25 0 1 0 429241814 95232000 22392 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23250 22392 603 41 0 23209 0
vsize: 93000
[startup+510.016 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 22899 0 0 0 50912 83 0 0 25 0 1 0 429241814 96694272 22737 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23607 22737 603 41 0 23566 0
vsize: 94428
[startup+520.016 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 23244 0 0 0 51911 84 0 0 25 0 1 0 429241814 98050048 23082 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23938 23082 603 41 0 23897 0
vsize: 95752
[startup+530.016 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 23597 0 0 0 52910 85 0 0 25 0 1 0 429241814 99528704 23435 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24299 23435 603 41 0 24258 0
vsize: 97196
[startup+540.017 s]
Raw data (loadavg): 0.99 0.84 0.45 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 23926 0 0 0 53909 87 0 0 25 0 1 0 429241814 100872192 23764 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24627 23764 603 41 0 24586 0
vsize: 98508
[startup+550.017 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24240 0 0 0 54907 88 0 0 25 0 1 0 429241814 102072320 24078 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24920 24078 603 41 0 24879 0
vsize: 99680
[startup+560.018 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24533 0 0 0 55906 89 0 0 25 0 1 0 429241814 103268352 24371 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25212 24371 603 41 0 25171 0
vsize: 100848
[startup+570.018 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 56906 89 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223824 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+580.019 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 57905 89 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+590.019 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 58905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+600.019 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 59905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134559853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+610.02 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 60905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+620.02 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 61904 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+630.02 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 62905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+640.02 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 63905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+650.019 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 64905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+660.019 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 65905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223792 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+670.019 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 66905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+680.02 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 67905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+690.019 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 68906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+700.019 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 69904 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+710.02 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 70905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+720.019 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 71905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+730.019 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 72905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+740.019 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 73905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+750.018 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 74905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+760.018 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 75905 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+770.018 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 76906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+780.019 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 77906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+790.019 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 78906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+800.018 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 79906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223776 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+810.019 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 80906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+820.019 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 81906 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223840 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+830.019 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 82907 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+840.019 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 83907 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+850.019 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 84907 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+860.019 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 85907 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+870.019 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 86907 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+880.019 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 87908 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+890.019 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 88908 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223840 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+900.019 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 89908 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+910.019 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 90908 90 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+920.02 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 91907 91 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+930.02 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24549 0 0 0 92907 91 0 0 25 0 1 0 429241814 103403520 24387 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24387 603 41 0 25204 0
vsize: 100980
[startup+940.02 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 93908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+950.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 94908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+960.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 95908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+970.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 96908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+980.021 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 97908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223744 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+990.021 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24550 0 0 0 98908 91 0 0 25 0 1 0 429241814 103403520 24388 4294967295 134512640 134672761 3221224640 3221223840 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24388 603 41 0 25204 0
vsize: 100980
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24551 0 0 0 99909 91 0 0 25 0 1 0 429241814 103403520 24389 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24389 603 41 0 25204 0
vsize: 100980
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24554 0 0 0 100909 91 0 0 25 0 1 0 429241814 103403520 24392 4294967295 134512640 134672761 3221224640 3221223744 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24392 603 41 0 25204 0
vsize: 100980
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24557 0 0 0 101909 91 0 0 25 0 1 0 429241814 103403520 24395 4294967295 134512640 134672761 3221224640 3221223744 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24395 603 41 0 25204 0
vsize: 100980
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24559 0 0 0 102909 91 0 0 25 0 1 0 429241814 103403520 24397 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24397 603 41 0 25204 0
vsize: 100980
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24562 0 0 0 103909 91 0 0 25 0 1 0 429241814 103403520 24400 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24400 603 41 0 25204 0
vsize: 100980
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24565 0 0 0 104909 91 0 0 25 0 1 0 429241814 103403520 24403 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24403 603 41 0 25204 0
vsize: 100980
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24568 0 0 0 105909 91 0 0 25 0 1 0 429241814 103403520 24406 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24406 603 41 0 25204 0
vsize: 100980
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24571 0 0 0 106910 91 0 0 25 0 1 0 429241814 103403520 24409 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24409 603 41 0 25204 0
vsize: 100980
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24574 0 0 0 107910 91 0 0 25 0 1 0 429241814 103403520 24412 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24412 603 41 0 25204 0
vsize: 100980
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24578 0 0 0 108910 91 0 0 25 0 1 0 429241814 103403520 24416 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24416 603 41 0 25204 0
vsize: 100980
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24580 0 0 0 109910 91 0 0 25 0 1 0 429241814 103403520 24418 4294967295 134512640 134672761 3221224640 3221223792 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25245 24418 603 41 0 25204 0
vsize: 100980
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24583 0 0 0 110910 91 0 0 25 0 1 0 429241814 103383040 24421 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25240 24421 603 41 0 25199 0
vsize: 100960
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24583 0 0 0 111911 91 0 0 25 0 1 0 429241814 103354368 24421 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24421 603 41 0 25192 0
vsize: 100932
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24583 0 0 0 112911 91 0 0 25 0 1 0 429241814 103354368 24421 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24421 603 41 0 25192 0
vsize: 100932
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24584 0 0 0 113911 91 0 0 25 0 1 0 429241814 103354368 24422 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24422 603 41 0 25192 0
vsize: 100932
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24584 0 0 0 114911 91 0 0 25 0 1 0 429241814 103354368 24422 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24422 603 41 0 25192 0
vsize: 100932
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24584 0 0 0 115911 91 0 0 25 0 1 0 429241814 103354368 24422 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24422 603 41 0 25192 0
vsize: 100932
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24584 0 0 0 116912 91 0 0 25 0 1 0 429241814 103354368 24422 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24422 603 41 0 25192 0
vsize: 100932
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24584 0 0 0 117912 91 0 0 25 0 1 0 429241814 103354368 24422 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24422 603 41 0 25192 0
vsize: 100932
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24585 0 0 0 118912 91 0 0 25 0 1 0 429241814 103354368 24423 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24423 603 41 0 25192 0
vsize: 100932
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 32409
Raw data (stat): 32409 (minisat+) R 32408 20937 20936 0 -1 0 24585 0 0 0 119912 91 0 0 25 0 1 0 429241814 103354368 24423 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25233 24423 603 41 0 25192 0
vsize: 100932
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 32409
Raw data (stat): 32409 (minisat+) Z 32408 20937 20936 0 -1 12 24588 0 0 0 119912 96 0 0 25 0 1 0 429241814 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.09
CPU user time (s): 1199.13
CPU system time (s): 0.966853
CPU usage (%): 100.002
Max. virtual memory (Kb): 100980
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####