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 6931

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        863472 kB
Buffers:         31920 kB
Cached:         119244 kB
SwapCached:          0 kB
Active:          51776 kB
Inactive:       102260 kB
HighTotal:      131008 kB
HighFree:         8428 kB
LowTotal:       903652 kB
LowFree:        855044 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11644 kB
Committed_AS:    63792 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:50:09 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 5004 7 1200.21 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.08 0.02 0.01 2/55 9316
Raw data (stat): 9316 (runsolver) R 9315 30927 30926 0 -1 64 3 0 0 0 0 0 0 0 19 0 1 0 364746580 1052672 98 4294967295 134512640 135381576 3221224448 3221219808 134891213 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 98 215 215 0 42 0
vsize: 1028
[startup+9.99966 s]
Raw data (loadavg): 0.22 0.05 0.02 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 5028 0 0 0 989 9 0 0 25 0 1 0 364746580 22913024 4866 4294967295 134512640 134672761 3221224560 3221223712 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5594 4866 603 41 0 5553 0
vsize: 22376
[startup+20.0003 s]
Raw data (loadavg): 0.34 0.08 0.02 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 5196 0 0 0 1988 10 0 0 25 0 1 0 364746580 23580672 5034 4294967295 134512640 134672761 3221224560 3221223712 134565143 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5757 5034 603 41 0 5716 0
vsize: 23028
[startup+29.9999 s]
Raw data (loadavg): 0.44 0.11 0.03 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 5437 0 0 0 2987 11 0 0 25 0 1 0 364746580 24653824 5275 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6019 5275 603 41 0 5978 0
vsize: 24076
[startup+40.0006 s]
Raw data (loadavg): 0.53 0.14 0.04 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 5673 0 0 0 3987 12 0 0 25 0 1 0 364746580 25636864 5511 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6259 5511 603 41 0 6218 0
vsize: 25036
[startup+50.0013 s]
Raw data (loadavg): 0.60 0.17 0.05 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 5997 0 0 0 4985 13 0 0 25 0 1 0 364746580 26963968 5835 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6583 5835 603 41 0 6542 0
vsize: 26332
[startup+60.0014 s]
Raw data (loadavg): 0.66 0.19 0.06 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 6256 0 0 0 5985 14 0 0 25 0 1 0 364746580 27910144 6094 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6814 6094 603 41 0 6773 0
vsize: 27256
[startup+70.0016 s]
Raw data (loadavg): 0.71 0.22 0.07 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 6566 0 0 0 6984 15 0 0 25 0 1 0 364746580 29237248 6404 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7138 6404 603 41 0 7097 0
vsize: 28552
[startup+80.0023 s]
Raw data (loadavg): 0.76 0.24 0.08 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 6842 0 0 0 7983 16 0 0 25 0 1 0 364746580 30441472 6680 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7432 6680 603 41 0 7391 0
vsize: 29728
[startup+90.0029 s]
Raw data (loadavg): 0.79 0.27 0.09 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 7268 0 0 0 8981 18 0 0 25 0 1 0 364746580 32190464 7106 4294967295 134512640 134672761 3221224560 3221223664 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7859 7106 603 41 0 7818 0
vsize: 31436
[startup+100.003 s]
Raw data (loadavg): 0.82 0.29 0.10 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 7625 0 0 0 9980 19 0 0 25 0 1 0 364746580 33665024 7463 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8219 7463 603 41 0 8178 0
vsize: 32876
[startup+110.002 s]
Raw data (loadavg): 0.85 0.31 0.11 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 7976 0 0 0 10979 20 0 0 25 0 1 0 364746580 35004416 7814 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8546 7814 603 41 0 8505 0
vsize: 34184
[startup+120.003 s]
Raw data (loadavg): 0.87 0.34 0.12 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 8341 0 0 0 11978 21 0 0 25 0 1 0 364746580 36605952 8179 4294967295 134512640 134672761 3221224560 3221223744 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8937 8179 603 41 0 8896 0
vsize: 35748
[startup+130.004 s]
Raw data (loadavg): 0.89 0.36 0.13 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 8682 0 0 0 12977 23 0 0 25 0 1 0 364746580 37949440 8520 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9265 8520 603 41 0 9224 0
vsize: 37060
[startup+140.004 s]
Raw data (loadavg): 0.91 0.38 0.14 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 9076 0 0 0 13975 24 0 0 25 0 1 0 364746580 39567360 8914 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9660 8914 603 41 0 9619 0
vsize: 38640
[startup+150.005 s]
Raw data (loadavg): 0.92 0.40 0.15 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 9438 0 0 0 14975 25 0 0 25 0 1 0 364746580 41041920 9276 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10020 9276 603 41 0 9979 0
vsize: 40080
[startup+160.005 s]
Raw data (loadavg): 0.93 0.42 0.15 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 9822 0 0 0 15973 26 0 0 25 0 1 0 364746580 42528768 9660 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10383 9660 603 41 0 10342 0
vsize: 41532
[startup+170.004 s]
Raw data (loadavg): 0.94 0.44 0.16 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 10180 0 0 0 16973 27 0 0 25 0 1 0 364746580 44011520 10018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10745 10018 603 41 0 10704 0
vsize: 42980
[startup+180.004 s]
Raw data (loadavg): 0.95 0.45 0.17 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 10504 0 0 0 17971 29 0 0 25 0 1 0 364746580 45359104 10342 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11074 10342 603 41 0 11033 0
vsize: 44296
[startup+190.005 s]
Raw data (loadavg): 0.96 0.47 0.18 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 10941 0 0 0 18970 30 0 0 25 0 1 0 364746580 47362048 10779 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11563 10779 603 41 0 11522 0
vsize: 46252
[startup+200.004 s]
Raw data (loadavg): 0.96 0.49 0.19 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 11585 0 0 0 19968 32 0 0 25 0 1 0 364746580 50057216 11423 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12221 11423 603 41 0 12180 0
vsize: 48884
[startup+210.004 s]
Raw data (loadavg): 0.97 0.51 0.20 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 12183 0 0 0 20966 34 0 0 25 0 1 0 364746580 52486144 12021 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12814 12021 603 41 0 12773 0
vsize: 51256
[startup+220.005 s]
Raw data (loadavg): 0.97 0.52 0.20 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 12730 0 0 0 21965 35 0 0 25 0 1 0 364746580 54640640 12568 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13340 12568 603 41 0 13299 0
vsize: 53360
[startup+230.004 s]
Raw data (loadavg): 0.98 0.54 0.21 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 13298 0 0 0 22963 37 0 0 25 0 1 0 364746580 57073664 13136 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13934 13136 603 41 0 13893 0
vsize: 55736
[startup+240.005 s]
Raw data (loadavg): 0.98 0.55 0.22 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 13871 0 0 0 23962 39 0 0 25 0 1 0 364746580 59359232 13709 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14492 13709 603 41 0 14451 0
vsize: 57968
[startup+250.006 s]
Raw data (loadavg): 0.98 0.57 0.23 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 14379 0 0 0 24961 40 0 0 25 0 1 0 364746580 61386752 14217 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14987 14217 603 41 0 14946 0
vsize: 59948
[startup+260.005 s]
Raw data (loadavg): 0.98 0.58 0.24 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 14881 0 0 0 25959 42 0 0 25 0 1 0 364746580 63549440 14719 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15515 14719 603 41 0 15474 0
vsize: 62060
[startup+270.005 s]
Raw data (loadavg): 0.99 0.59 0.24 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 15338 0 0 0 26958 44 0 0 25 0 1 0 364746580 65327104 15176 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15949 15176 603 41 0 15908 0
vsize: 63796
[startup+280.004 s]
Raw data (loadavg): 0.99 0.61 0.25 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 15743 0 0 0 27957 45 0 0 25 0 1 0 364746580 67076096 15581 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16376 15581 603 41 0 16335 0
vsize: 65504
[startup+290.005 s]
Raw data (loadavg): 0.99 0.62 0.26 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 15943 0 0 0 28956 46 0 0 25 0 1 0 364746580 67883008 15781 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16573 15781 603 41 0 16532 0
vsize: 66292
[startup+300.005 s]
Raw data (loadavg): 0.99 0.63 0.27 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 16336 0 0 0 29955 47 0 0 25 0 1 0 364746580 69488640 16174 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16965 16174 603 41 0 16924 0
vsize: 67860
[startup+310.005 s]
Raw data (loadavg): 0.99 0.64 0.28 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 16684 0 0 0 30954 48 0 0 25 0 1 0 364746580 70832128 16522 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17293 16522 603 41 0 17252 0
vsize: 69172
[startup+320.004 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 16987 0 0 0 31953 49 0 0 25 0 1 0 364746580 72167424 16825 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17619 16825 603 41 0 17578 0
vsize: 70476
[startup+330.005 s]
Raw data (loadavg): 0.99 0.66 0.29 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 17112 0 0 0 32953 50 0 0 25 0 1 0 364746580 72572928 16950 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17718 16950 603 41 0 17677 0
vsize: 70872
[startup+340.006 s]
Raw data (loadavg): 0.99 0.67 0.30 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 17253 0 0 0 33952 50 0 0 25 0 1 0 364746580 73248768 17091 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17883 17091 603 41 0 17842 0
vsize: 71532
[startup+350.005 s]
Raw data (loadavg): 0.99 0.68 0.30 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 17551 0 0 0 34951 51 0 0 25 0 1 0 364746580 74452992 17389 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18177 17389 603 41 0 18136 0
vsize: 72708
[startup+360.005 s]
Raw data (loadavg): 0.99 0.69 0.31 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 17979 0 0 0 35950 53 0 0 25 0 1 0 364746580 76189696 17817 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18601 17817 603 41 0 18560 0
vsize: 74404
[startup+370.006 s]
Raw data (loadavg): 0.99 0.70 0.32 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 18407 0 0 0 36948 55 0 0 25 0 1 0 364746580 77938688 18245 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19028 18245 603 41 0 18987 0
vsize: 76112
[startup+380.005 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 18827 0 0 0 37947 56 0 0 25 0 1 0 364746580 79667200 18665 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 18665 603 41 0 19409 0
vsize: 77800
[startup+390.006 s]
Raw data (loadavg): 0.99 0.72 0.33 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 19086 0 0 0 38946 58 0 0 25 0 1 0 364746580 80613376 18924 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19681 18924 603 41 0 19640 0
vsize: 78724
[startup+400.006 s]
Raw data (loadavg): 0.99 0.73 0.34 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 19522 0 0 0 39945 59 0 0 25 0 1 0 364746580 82358272 19360 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20107 19360 603 41 0 20066 0
vsize: 80428
[startup+410.005 s]
Raw data (loadavg): 0.99 0.74 0.34 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 19767 0 0 0 40944 60 0 0 25 0 1 0 364746580 83423232 19605 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20367 19605 603 41 0 20326 0
vsize: 81468
[startup+420.005 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 19923 0 0 0 41943 60 0 0 25 0 1 0 364746580 84496384 19761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20629 19761 603 41 0 20588 0
vsize: 82516
[startup+430.006 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 20146 0 0 0 42942 61 0 0 25 0 1 0 364746580 85438464 19984 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20859 19984 603 41 0 20818 0
vsize: 83436
[startup+440.006 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 20513 0 0 0 43941 63 0 0 25 0 1 0 364746580 86917120 20351 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21220 20351 603 41 0 21179 0
vsize: 84880
[startup+450.006 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 20875 0 0 0 44939 65 0 0 25 0 1 0 364746580 88391680 20713 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21580 20713 603 41 0 21539 0
vsize: 86320
[startup+460.006 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 21299 0 0 0 45938 66 0 0 25 0 1 0 364746580 90132480 21137 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22005 21137 603 41 0 21964 0
vsize: 88020
[startup+470.005 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 21662 0 0 0 46936 68 0 0 25 0 1 0 364746580 91611136 21500 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22366 21500 603 41 0 22325 0
vsize: 89464
[startup+480.005 s]
Raw data (loadavg): 0.99 0.79 0.39 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 22036 0 0 0 47935 69 0 0 25 0 1 0 364746580 93089792 21874 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22727 21874 603 41 0 22686 0
vsize: 90908
[startup+490.006 s]
Raw data (loadavg): 0.99 0.80 0.39 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 22389 0 0 0 48934 70 0 0 25 0 1 0 364746580 94556160 22227 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23085 22227 603 41 0 23044 0
vsize: 92340
[startup+500.005 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 22740 0 0 0 49932 72 0 0 25 0 1 0 364746580 96043008 22578 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23448 22578 603 41 0 23407 0
vsize: 93792
[startup+510.005 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 23099 0 0 0 50932 73 0 0 25 0 1 0 364746580 97513472 22937 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23807 22937 603 41 0 23766 0
vsize: 95228
[startup+520.005 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 23448 0 0 0 51931 74 0 0 25 0 1 0 364746580 98844672 23286 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24132 23286 603 41 0 24091 0
vsize: 96528
[startup+530.005 s]
Raw data (loadavg): 0.99 0.82 0.42 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 23779 0 0 0 52929 75 0 0 25 0 1 0 364746580 100179968 23617 4294967295 134512640 134672761 3221224560 3221223664 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24458 23617 603 41 0 24417 0
vsize: 97832
[startup+540.006 s]
Raw data (loadavg): 0.99 0.83 0.42 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24109 0 0 0 53928 77 0 0 25 0 1 0 364746580 101515264 23947 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24784 23947 603 41 0 24743 0
vsize: 99136
[startup+550.007 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24398 0 0 0 54927 78 0 0 25 0 1 0 364746580 102723584 24236 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25079 24236 603 41 0 25038 0
vsize: 100316
[startup+560.006 s]
Raw data (loadavg): 0.99 0.84 0.43 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 55927 79 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+570.006 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 56926 79 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+580.006 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 57926 79 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+590.006 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 58927 79 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+600.008 s]
Raw data (loadavg): 0.99 0.85 0.46 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 59926 79 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223760 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+610.007 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 60926 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+620.006 s]
Raw data (loadavg): 0.99 0.86 0.47 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 61926 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+630.007 s]
Raw data (loadavg): 0.99 0.87 0.47 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 62926 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+640.008 s]
Raw data (loadavg): 0.99 0.87 0.48 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 63926 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134560396 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+650.008 s]
Raw data (loadavg): 0.99 0.87 0.48 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 64927 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+660.008 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 65926 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+670.008 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 66927 80 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+680.008 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 67926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+690.008 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 68926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134559802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+700.009 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 69926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+710.009 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 70927 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+720.009 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 71926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+730.009 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 72926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+740.01 s]
Raw data (loadavg): 0.99 0.90 0.53 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 73926 81 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+750.009 s]
Raw data (loadavg): 0.99 0.91 0.53 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 74926 82 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+760.009 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 75926 82 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+770.01 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 76926 82 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+780.01 s]
Raw data (loadavg): 0.99 0.91 0.55 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 77926 82 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+790.01 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 78926 82 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+800.011 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 79926 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+810.01 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 80926 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+820.01 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 81926 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223696 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+830.011 s]
Raw data (loadavg): 0.99 0.92 0.57 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 82926 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+840.012 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 83925 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+850.012 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 84925 83 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+860.012 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 85925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+870.012 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 86925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+880.012 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 87925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+890.013 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 88925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223664 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+900.014 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 89925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+910.013 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24517 0 0 0 90925 84 0 0 25 0 1 0 364746580 103260160 24355 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24355 603 41 0 25169 0
vsize: 100840
[startup+920.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 91926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+930.014 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 92926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+940.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 93926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+950.015 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 94926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+960.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 95926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+970.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 96926 84 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+980.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24518 0 0 0 97926 85 0 0 25 0 1 0 364746580 103260160 24356 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24356 603 41 0 25169 0
vsize: 100840
[startup+990.016 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24521 0 0 0 98926 85 0 0 25 0 1 0 364746580 103260160 24359 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24359 603 41 0 25169 0
vsize: 100840
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24525 0 0 0 99927 85 0 0 25 0 1 0 364746580 103260160 24363 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24363 603 41 0 25169 0
vsize: 100840
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24527 0 0 0 100927 86 0 0 25 0 1 0 364746580 103260160 24365 4294967295 134512640 134672761 3221224560 3221223744 134559392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24365 603 41 0 25169 0
vsize: 100840
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24529 0 0 0 101927 86 0 0 25 0 1 0 364746580 103260160 24367 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24367 603 41 0 25169 0
vsize: 100840
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24532 0 0 0 102927 86 0 0 25 0 1 0 364746580 103260160 24370 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24370 603 41 0 25169 0
vsize: 100840
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24535 0 0 0 103927 86 0 0 25 0 1 0 364746580 103260160 24373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24373 603 41 0 25169 0
vsize: 100840
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24538 0 0 0 104927 86 0 0 25 0 1 0 364746580 103260160 24376 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24376 603 41 0 25169 0
vsize: 100840
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24541 0 0 0 105927 86 0 0 25 0 1 0 364746580 103260160 24379 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24379 603 41 0 25169 0
vsize: 100840
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24545 0 0 0 106927 86 0 0 25 0 1 0 364746580 103260160 24383 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24383 603 41 0 25169 0
vsize: 100840
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24548 0 0 0 107927 86 0 0 25 0 1 0 364746580 103260160 24386 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24386 603 41 0 25169 0
vsize: 100840
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24551 0 0 0 108927 86 0 0 25 0 1 0 364746580 103260160 24389 4294967295 134512640 134672761 3221224560 3221222608 134565775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24389 603 41 0 25169 0
vsize: 100840
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24551 0 0 0 109927 87 0 0 25 0 1 0 364746580 103260160 24389 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24389 603 41 0 25169 0
vsize: 100840
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24551 0 0 0 110927 87 0 0 25 0 1 0 364746580 103260160 24389 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24389 603 41 0 25169 0
vsize: 100840
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 111927 87 0 0 25 0 1 0 364746580 103260160 24390 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24390 603 41 0 25169 0
vsize: 100840
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 112927 87 0 0 25 0 1 0 364746580 103260160 24390 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24390 603 41 0 25169 0
vsize: 100840
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 113927 87 0 0 25 0 1 0 364746580 103260160 24390 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24390 603 41 0 25169 0
vsize: 100840
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 114927 87 0 0 25 0 1 0 364746580 103260160 24390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25210 24390 603 41 0 25169 0
vsize: 100840
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 115927 87 0 0 25 0 1 0 364746580 103243776 24390 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25206 24390 603 41 0 25165 0
vsize: 100824
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 116927 87 0 0 25 0 1 0 364746580 103243776 24390 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25206 24390 603 41 0 25165 0
vsize: 100824
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 117927 87 0 0 25 0 1 0 364746580 103243776 24390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25206 24390 603 41 0 25165 0
vsize: 100824
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 118927 87 0 0 25 0 1 0 364746580 103243776 24390 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25206 24390 603 41 0 25165 0
vsize: 100824
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 9316
Raw data (stat): 9316 (minisat+) R 9315 30927 30926 0 -1 0 24552 0 0 0 119928 87 0 0 25 0 1 0 364746580 103243776 24390 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25206 24390 603 41 0 25165 0
vsize: 100824
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.69 1/55 9316
Raw data (stat): 9316 (minisat+) Z 9315 30927 30926 0 -1 12 24555 0 0 0 119928 92 0 0 25 0 1 0 364746580 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.08
CPU time (s): 1200.21
CPU user time (s): 1199.28
CPU system time (s): 0.924859
CPU usage (%): 100.011
Max. virtual memory (Kb): 100840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####