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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/een/normalized-seymour.opb
MD5SUM23a177449585151350479e80b33e6416
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
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 numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1.04984
Number of variables1255
Total number of constraints4827
Number of constraints which are clauses4827
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint19

Trace number 6932 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc22 THE 2005-04-14 20:30:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5005 boxname=wulflinc22 idbench=385 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  23a177449585151350479e80b33e6416  /oldhome/oroussel/tmp/wulflinc22/normalized-seymour.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc22/normalized-seymour.opb /oldhome/oroussel/tmp/wulflinc22/normalized-seymour.opb
IDLAUNCH: 5005
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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.031
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:        820260 kB
Buffers:         34920 kB
Cached:         136392 kB
SwapCached:        524 kB
Active:          56960 kB
Inactive:       117720 kB
HighTotal:      131008 kB
HighFree:          812 kB
LowTotal:       903652 kB
LowFree:        819448 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            34236 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:50:10 (client local time) WITH STATUS 10 IN 1200.09 SECONDS
stats: 5005 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 Found solution: 349
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 |  192498   472283 |   64166       0        0     nan |  0.000 % |
c |       102 |  192472   472225 |   70582     101      757     7.5 |  0.013 % |
c |       252 |  191986   471124 |   77640     243     1396     5.7 |  0.225 % |
c |       478 |  191727   470532 |   85404     461     2485     5.4 |  0.347 % |
c |       815 |  191000   468880 |   93945     788     4650     5.9 |  0.670 % |
c |      1321 |  187783   461507 |  103339    1229     7075     5.8 |  2.192 % |
c |      2081 |  184476   453937 |  113673    1935    11794     6.1 |  3.744 % |
c |      3220 |  183263   451163 |  125041    3036    18174     6.0 |  4.332 % |
c |      4928 |  179727   443024 |  137545    4623    31025     6.7 |  6.023 % |
c |      7490 |  176123   434697 |  151300    6910    47688     6.9 |  7.799 % |
c |     11336 |  175071   432245 |  166430   10714    75355     7.0 |  8.309 % |
c |     17102 |  174660   431288 |  183073   16452   125760     7.6 |  8.511 % |
c |     25751 |  173356   428252 |  201380   25023   204102     8.2 |  9.138 % |
c |     38725 |  173292   428104 |  221518   37975   365675     9.6 |  9.170 % |
c |     58192 |  172399   426023 |  243670   57325   787940    13.7 |  9.597 % |
c |     87385 |  172143   425423 |  268037   86440  1552741    18.0 |  9.723 % |
c |    131175 |  171419   423726 |  294841  130057  2669383    20.5 | 10.082 % |
c |    196859 |  170875   422450 |  324325  195501  6623630    33.9 | 10.349 % |
c |    295386 |  170757   422174 |  356757  293931 11098865    37.8 | 10.408 % |
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.00 0.00 0.00 2/54 2988
Raw data (stat): 2988 (runsolver) R 2987 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487481532 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 5636 0 0 0 983 14 0 0 25 0 1 0 487481532 25563136 5505 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6241 5505 603 41 0 6200 0
vsize: 24964
[startup+19.9998 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 5679 0 0 0 1972 14 0 0 25 0 1 0 487481532 25702400 5548 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6275 5548 603 41 0 6234 0
vsize: 25100
[startup+30.0008 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 5844 0 0 0 2972 14 0 0 25 0 1 0 487481532 26411008 5713 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6448 5713 603 41 0 6407 0
vsize: 25792
[startup+40.0009 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 5951 0 0 0 3971 15 0 0 25 0 1 0 487481532 26816512 5820 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6547 5820 603 41 0 6506 0
vsize: 26188
[startup+50.0018 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6138 0 0 0 4971 15 0 0 25 0 1 0 487481532 27615232 6007 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6742 6007 603 41 0 6701 0
vsize: 26968
[startup+60.0018 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6340 0 0 0 5971 16 0 0 25 0 1 0 487481532 28422144 6209 4294967295 134512640 134672761 3221224560 3221223760 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6939 6209 603 41 0 6898 0
vsize: 27756
[startup+70.0012 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6532 0 0 0 6970 16 0 0 25 0 1 0 487481532 29224960 6401 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7135 6401 603 41 0 7094 0
vsize: 28540
[startup+80.0022 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6689 0 0 0 7970 17 0 0 25 0 1 0 487481532 29761536 6558 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7266 6558 603 41 0 7225 0
vsize: 29064
[startup+90.0019 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6812 0 0 0 8969 18 0 0 25 0 1 0 487481532 30298112 6681 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7397 6681 603 41 0 7356 0
vsize: 29588
[startup+100.002 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 6955 0 0 0 9969 18 0 0 25 0 1 0 487481532 30830592 6824 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7527 6824 603 41 0 7486 0
vsize: 30108
[startup+110.004 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7105 0 0 0 10969 19 0 0 25 0 1 0 487481532 31756288 6974 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7753 6974 603 41 0 7712 0
vsize: 31012
[startup+120.004 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7276 0 0 0 11969 19 0 0 25 0 1 0 487481532 32423936 7145 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7916 7145 603 41 0 7875 0
vsize: 31664
[startup+130.004 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7418 0 0 0 12968 20 0 0 25 0 1 0 487481532 32964608 7287 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8048 7287 603 41 0 8007 0
vsize: 32192
[startup+140.004 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7527 0 0 0 13968 20 0 0 25 0 1 0 487481532 33366016 7396 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8146 7396 603 41 0 8105 0
vsize: 32584
[startup+150.005 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7608 0 0 0 14969 20 0 0 25 0 1 0 487481532 33767424 7477 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8244 7477 603 41 0 8203 0
vsize: 32976
[startup+160.004 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7695 0 0 0 15969 20 0 0 25 0 1 0 487481532 34033664 7564 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8309 7564 603 41 0 8268 0
vsize: 33236
[startup+170.005 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7857 0 0 0 16968 20 0 0 25 0 1 0 487481532 34709504 7726 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8474 7726 603 41 0 8433 0
vsize: 33896
[startup+180.005 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 7948 0 0 0 17967 21 0 0 25 0 1 0 487481532 35110912 7817 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8572 7817 603 41 0 8531 0
vsize: 34288
[startup+190.005 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8109 0 0 0 18966 22 0 0 25 0 1 0 487481532 35647488 7978 4294967295 134512640 134672761 3221224560 3221223728 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8703 7978 603 41 0 8662 0
vsize: 34812
[startup+200.006 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8234 0 0 0 19966 22 0 0 25 0 1 0 487481532 36188160 8103 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8835 8103 603 41 0 8794 0
vsize: 35340
[startup+210.006 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8390 0 0 0 20965 23 0 0 25 0 1 0 487481532 36859904 8259 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8999 8259 603 41 0 8958 0
vsize: 35996
[startup+220.006 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8492 0 0 0 21964 23 0 0 25 0 1 0 487481532 37265408 8361 4294967295 134512640 134672761 3221224560 3221223760 134557922 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9098 8361 603 41 0 9057 0
vsize: 36392
[startup+230.006 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8550 0 0 0 22965 23 0 0 25 0 1 0 487481532 37400576 8419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9131 8419 603 41 0 9090 0
vsize: 36524
[startup+240.006 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8612 0 0 0 23964 24 0 0 25 0 1 0 487481532 37670912 8481 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9197 8481 603 41 0 9156 0
vsize: 36788
[startup+250.007 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8675 0 0 0 24964 24 0 0 25 0 1 0 487481532 37937152 8544 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9262 8544 603 41 0 9221 0
vsize: 37048
[startup+260.007 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8749 0 0 0 25964 24 0 0 25 0 1 0 487481532 38199296 8618 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9326 8618 603 41 0 9285 0
vsize: 37304
[startup+270.006 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8818 0 0 0 26964 25 0 0 25 0 1 0 487481532 38461440 8687 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9390 8687 603 41 0 9349 0
vsize: 37560
[startup+280.007 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 8901 0 0 0 27964 25 0 0 25 0 1 0 487481532 38862848 8770 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9488 8770 603 41 0 9447 0
vsize: 37952
[startup+290.007 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9026 0 0 0 28964 25 0 0 25 0 1 0 487481532 39399424 8895 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9619 8895 603 41 0 9578 0
vsize: 38476
[startup+300.007 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9114 0 0 0 29964 25 0 0 25 0 1 0 487481532 39665664 8983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9684 8983 603 41 0 9643 0
vsize: 38736
[startup+310.007 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9213 0 0 0 30964 26 0 0 25 0 1 0 487481532 40062976 9082 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9082 603 41 0 9740 0
vsize: 39124
[startup+320.007 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9347 0 0 0 31963 26 0 0 25 0 1 0 487481532 40595456 9216 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9911 9216 603 41 0 9870 0
vsize: 39644
[startup+330.008 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9459 0 0 0 32962 27 0 0 25 0 1 0 487481532 41656320 9328 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10170 9328 603 41 0 10129 0
vsize: 40680
[startup+340.008 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9559 0 0 0 33962 27 0 0 25 0 1 0 487481532 42057728 9428 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10268 9428 603 41 0 10227 0
vsize: 41072
[startup+350.009 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9721 0 0 0 34961 28 0 0 25 0 1 0 487481532 42594304 9590 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10399 9590 603 41 0 10358 0
vsize: 41596
[startup+360.01 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9829 0 0 0 35961 29 0 0 25 0 1 0 487481532 43134976 9698 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10531 9698 603 41 0 10490 0
vsize: 42124
[startup+370.009 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 9967 0 0 0 36961 29 0 0 25 0 1 0 487481532 43671552 9836 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10662 9836 603 41 0 10621 0
vsize: 42648
[startup+380.009 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10050 0 0 0 37961 29 0 0 25 0 1 0 487481532 43937792 9919 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10727 9919 603 41 0 10686 0
vsize: 42908
[startup+390.01 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10163 0 0 0 38960 30 0 0 25 0 1 0 487481532 44478464 10032 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10859 10032 603 41 0 10818 0
vsize: 43436
[startup+400.01 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10305 0 0 0 39960 31 0 0 25 0 1 0 487481532 45006848 10174 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10988 10174 603 41 0 10947 0
vsize: 43952
[startup+410.01 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10418 0 0 0 40960 31 0 0 25 0 1 0 487481532 45412352 10287 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11087 10287 603 41 0 11046 0
vsize: 44348
[startup+420.01 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10578 0 0 0 41960 31 0 0 25 0 1 0 487481532 46075904 10447 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11249 10447 603 41 0 11208 0
vsize: 44996
[startup+430.01 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10723 0 0 0 42959 32 0 0 25 0 1 0 487481532 46743552 10592 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11412 10592 603 41 0 11371 0
vsize: 45648
[startup+440.01 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 10839 0 0 0 43959 32 0 0 25 0 1 0 487481532 47144960 10708 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11510 10708 603 41 0 11469 0
vsize: 46040
[startup+450.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11000 0 0 0 44959 32 0 0 25 0 1 0 487481532 47812608 10869 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11673 10869 603 41 0 11632 0
vsize: 46692
[startup+460.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11197 0 0 0 45959 33 0 0 25 0 1 0 487481532 48611328 11066 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11868 11066 603 41 0 11827 0
vsize: 47472
[startup+470.011 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11343 0 0 0 46959 33 0 0 25 0 1 0 487481532 49283072 11212 4294967295 134512640 134672761 3221224560 3221223728 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12032 11212 603 41 0 11991 0
vsize: 48128
[startup+480.012 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11490 0 0 0 47959 33 0 0 25 0 1 0 487481532 49819648 11359 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12163 11359 603 41 0 12122 0
vsize: 48652
[startup+490.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11708 0 0 0 48958 34 0 0 25 0 1 0 487481532 50761728 11577 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12393 11577 603 41 0 12352 0
vsize: 49572
[startup+500.012 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11870 0 0 0 49958 34 0 0 25 0 1 0 487481532 51437568 11739 4294967295 134512640 134672761 3221224560 3221223696 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12558 11739 603 41 0 12517 0
vsize: 50232
[startup+510.013 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 11989 0 0 0 50958 34 0 0 25 0 1 0 487481532 51838976 11858 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12656 11858 603 41 0 12615 0
vsize: 50624
[startup+520.012 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12172 0 0 0 51958 35 0 0 25 0 1 0 487481532 52649984 12041 4294967295 134512640 134672761 3221224560 3221223696 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12854 12041 603 41 0 12813 0
vsize: 51416
[startup+530.014 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12348 0 0 0 52957 36 0 0 25 0 1 0 487481532 53321728 12217 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13018 12217 603 41 0 12977 0
vsize: 52072
[startup+540.014 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12433 0 0 0 53957 36 0 0 25 0 1 0 487481532 53727232 12302 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13117 12302 603 41 0 13076 0
vsize: 52468
[startup+550.014 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12540 0 0 0 54957 36 0 0 25 0 1 0 487481532 54128640 12409 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13215 12409 603 41 0 13174 0
vsize: 52860
[startup+560.014 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12675 0 0 0 55956 37 0 0 25 0 1 0 487481532 54669312 12544 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13347 12544 603 41 0 13306 0
vsize: 53388
[startup+570.014 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12820 0 0 0 56956 38 0 0 25 0 1 0 487481532 55205888 12689 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13478 12689 603 41 0 13437 0
vsize: 53912
[startup+580.015 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 12960 0 0 0 57956 38 0 0 25 0 1 0 487481532 55889920 12829 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13645 12829 603 41 0 13604 0
vsize: 54580
[startup+590.015 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13011 0 0 0 58956 38 0 0 25 0 1 0 487481532 56020992 12880 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13677 12880 603 41 0 13636 0
vsize: 54708
[startup+600.016 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13084 0 0 0 59956 39 0 0 25 0 1 0 487481532 56291328 12953 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13743 12953 603 41 0 13702 0
vsize: 54972
[startup+610.017 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13178 0 0 0 60956 39 0 0 25 0 1 0 487481532 56692736 13047 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13841 13047 603 41 0 13800 0
vsize: 55364
[startup+620.017 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13314 0 0 0 61956 39 0 0 25 0 1 0 487481532 57229312 13183 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13972 13183 603 41 0 13931 0
vsize: 55888
[startup+630.017 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13382 0 0 0 62956 40 0 0 25 0 1 0 487481532 57499648 13251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14038 13251 603 41 0 13997 0
vsize: 56152
[startup+640.018 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13475 0 0 0 63955 40 0 0 25 0 1 0 487481532 57896960 13344 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14135 13344 603 41 0 14094 0
vsize: 56540
[startup+650.019 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13839 0 0 0 64955 41 0 0 25 0 1 0 487481532 59371520 13708 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14495 13708 603 41 0 14454 0
vsize: 57980
[startup+660.02 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 13954 0 0 0 65954 41 0 0 25 0 1 0 487481532 59772928 13823 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14593 13823 603 41 0 14552 0
vsize: 58372
[startup+670.02 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14144 0 0 0 66953 42 0 0 25 0 1 0 487481532 60575744 14013 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14789 14013 603 41 0 14748 0
vsize: 59156
[startup+680.021 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14212 0 0 0 67953 43 0 0 25 0 1 0 487481532 60850176 14081 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14856 14081 603 41 0 14815 0
vsize: 59424
[startup+690.021 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14303 0 0 0 68952 43 0 0 25 0 1 0 487481532 61251584 14172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14954 14172 603 41 0 14913 0
vsize: 59816
[startup+700.021 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14366 0 0 0 69952 43 0 0 25 0 1 0 487481532 61517824 14235 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15019 14235 603 41 0 14978 0
vsize: 60076
[startup+710.022 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14460 0 0 0 70953 43 0 0 25 0 1 0 487481532 61788160 14329 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15085 14329 603 41 0 15044 0
vsize: 60340
[startup+720.022 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14550 0 0 0 71952 44 0 0 25 0 1 0 487481532 62189568 14419 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15183 14419 603 41 0 15142 0
vsize: 60732
[startup+730.022 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14667 0 0 0 72953 44 0 0 25 0 1 0 487481532 62590976 14536 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15281 14536 603 41 0 15240 0
vsize: 61124
[startup+740.023 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14764 0 0 0 73953 44 0 0 25 0 1 0 487481532 62992384 14633 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15379 14633 603 41 0 15338 0
vsize: 61516
[startup+750.024 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 14928 0 0 0 74953 44 0 0 25 0 1 0 487481532 63655936 14797 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15541 14797 603 41 0 15500 0
vsize: 62164
[startup+760.024 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15074 0 0 0 75952 45 0 0 25 0 1 0 487481532 64331776 14943 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15706 14943 603 41 0 15665 0
vsize: 62824
[startup+770.023 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15242 0 0 0 76952 45 0 0 25 0 1 0 487481532 65007616 15111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15871 15111 603 41 0 15830 0
vsize: 63484
[startup+780.024 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15413 0 0 0 77952 45 0 0 25 0 1 0 487481532 65683456 15282 4294967295 134512640 134672761 3221224560 3221223728 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16036 15282 603 41 0 15995 0
vsize: 64144
[startup+790.024 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15572 0 0 0 78952 45 0 0 25 0 1 0 487481532 66355200 15441 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16200 15441 603 41 0 16159 0
vsize: 64800
[startup+800.024 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15713 0 0 0 79952 45 0 0 25 0 1 0 487481532 66891776 15582 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16331 15582 603 41 0 16290 0
vsize: 65324
[startup+810.025 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 15878 0 0 0 80952 46 0 0 25 0 1 0 487481532 67563520 15747 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16495 15747 603 41 0 16454 0
vsize: 65980
[startup+820.025 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16035 0 0 0 81952 46 0 0 25 0 1 0 487481532 68235264 15904 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16659 15904 603 41 0 16618 0
vsize: 66636
[startup+830.025 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16200 0 0 0 82952 47 0 0 25 0 1 0 487481532 68907008 16069 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16823 16069 603 41 0 16782 0
vsize: 67292
[startup+840.025 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16391 0 0 0 83951 48 0 0 25 0 1 0 487481532 69705728 16260 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17018 16260 603 41 0 16977 0
vsize: 68072
[startup+850.025 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16523 0 0 0 84951 48 0 0 25 0 1 0 487481532 70246400 16392 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17150 16392 603 41 0 17109 0
vsize: 68600
[startup+860.024 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16652 0 0 0 85951 48 0 0 25 0 1 0 487481532 70647808 16521 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17248 16521 603 41 0 17207 0
vsize: 68992
[startup+870.024 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16805 0 0 0 86950 49 0 0 25 0 1 0 487481532 71315456 16674 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17411 16674 603 41 0 17370 0
vsize: 69644
[startup+880.025 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 16915 0 0 0 87950 49 0 0 25 0 1 0 487481532 71716864 16784 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16784 603 41 0 17468 0
vsize: 70036
[startup+890.025 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17069 0 0 0 88950 50 0 0 25 0 1 0 487481532 72384512 16938 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17672 16938 603 41 0 17631 0
vsize: 70688
[startup+900.024 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17150 0 0 0 89949 50 0 0 25 0 1 0 487481532 72650752 17019 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17737 17019 603 41 0 17696 0
vsize: 70948
[startup+910.024 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17237 0 0 0 90949 50 0 0 25 0 1 0 487481532 73056256 17106 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17836 17106 603 41 0 17795 0
vsize: 71344
[startup+920.023 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17343 0 0 0 91949 51 0 0 25 0 1 0 487481532 73461760 17212 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17935 17212 603 41 0 17894 0
vsize: 71740
[startup+930.023 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17437 0 0 0 92949 51 0 0 25 0 1 0 487481532 73859072 17306 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18032 17306 603 41 0 17991 0
vsize: 72128
[startup+940.023 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17506 0 0 0 93949 51 0 0 25 0 1 0 487481532 74129408 17375 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18098 17375 603 41 0 18057 0
vsize: 72392
[startup+950.023 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17618 0 0 0 94949 52 0 0 25 0 1 0 487481532 74657792 17487 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18227 17487 603 41 0 18186 0
vsize: 72908
[startup+960.024 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17737 0 0 0 95949 52 0 0 25 0 1 0 487481532 75063296 17606 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18326 17606 603 41 0 18285 0
vsize: 73304
[startup+970.023 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17834 0 0 0 96949 52 0 0 25 0 1 0 487481532 75464704 17703 4294967295 134512640 134672761 3221224560 3221223728 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18424 17703 603 41 0 18383 0
vsize: 73696
[startup+980.024 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 17915 0 0 0 97949 52 0 0 25 0 1 0 487481532 75870208 17784 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18523 17784 603 41 0 18482 0
vsize: 74092
[startup+990.025 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18004 0 0 0 98948 53 0 0 25 0 1 0 487481532 77189120 17873 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18845 17873 603 41 0 18804 0
vsize: 75380
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18101 0 0 0 99948 53 0 0 25 0 1 0 487481532 77590528 17970 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18943 17970 603 41 0 18902 0
vsize: 75772
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18189 0 0 0 100948 53 0 0 25 0 1 0 487481532 77987840 18058 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19040 18058 603 41 0 18999 0
vsize: 76160
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18263 0 0 0 101948 54 0 0 25 0 1 0 487481532 78258176 18132 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19106 18132 603 41 0 19065 0
vsize: 76424
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18351 0 0 0 102948 54 0 0 25 0 1 0 487481532 78663680 18220 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19205 18220 603 41 0 19164 0
vsize: 76820
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18440 0 0 0 103948 54 0 0 25 0 1 0 487481532 78925824 18309 4294967295 134512640 134672761 3221224560 3221223664 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19269 18309 603 41 0 19228 0
vsize: 77076
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18549 0 0 0 104948 55 0 0 25 0 1 0 487481532 79331328 18418 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19368 18418 603 41 0 19327 0
vsize: 77472
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18635 0 0 0 105948 55 0 0 25 0 1 0 487481532 79732736 18504 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19466 18504 603 41 0 19425 0
vsize: 77864
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18730 0 0 0 106948 55 0 0 25 0 1 0 487481532 80125952 18599 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19562 18599 603 41 0 19521 0
vsize: 78248
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18829 0 0 0 107948 55 0 0 25 0 1 0 487481532 80531456 18698 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19661 18698 603 41 0 19620 0
vsize: 78644
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 18914 0 0 0 108948 56 0 0 25 0 1 0 487481532 80801792 18783 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19727 18783 603 41 0 19686 0
vsize: 78908
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19007 0 0 0 109948 56 0 0 25 0 1 0 487481532 81211392 18876 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19827 18876 603 41 0 19786 0
vsize: 79308
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19121 0 0 0 110948 56 0 0 25 0 1 0 487481532 81739776 18990 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19956 18990 603 41 0 19915 0
vsize: 79824
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19259 0 0 0 111947 57 0 0 25 0 1 0 487481532 82305024 19128 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20094 19128 603 41 0 20053 0
vsize: 80376
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19367 0 0 0 112947 57 0 0 25 0 1 0 487481532 82702336 19236 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20191 19236 603 41 0 20150 0
vsize: 80764
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19489 0 0 0 113945 58 0 0 25 0 1 0 487481532 83103744 19358 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20289 19358 603 41 0 20248 0
vsize: 81156
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19561 0 0 0 114946 58 0 0 25 0 1 0 487481532 83509248 19430 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20388 19430 603 41 0 20347 0
vsize: 81552
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19686 0 0 0 115945 58 0 0 25 0 1 0 487481532 83914752 19555 4294967295 134512640 134672761 3221224560 3221223728 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20487 19555 603 41 0 20446 0
vsize: 81948
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19757 0 0 0 116945 59 0 0 25 0 1 0 487481532 84180992 19626 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20552 19626 603 41 0 20511 0
vsize: 82208
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19873 0 0 0 117945 59 0 0 25 0 1 0 487481532 84717568 19742 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20683 19742 603 41 0 20642 0
vsize: 82732
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 19969 0 0 0 118945 59 0 0 25 0 1 0 487481532 85114880 19838 4294967295 134512640 134672761 3221224560 3221223664 134560207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20780 19838 603 41 0 20739 0
vsize: 83120
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 2988
Raw data (stat): 2988 (minisat+) R 2987 26298 26297 0 -1 0 20077 0 0 0 119945 59 0 0 25 0 1 0 487481532 85512192 19946 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20877 19946 603 41 0 20836 0
vsize: 83508
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 2988
Raw data (stat): 2988 (minisat+) Z 2987 26298 26297 0 -1 12 20080 0 0 0 119945 63 0 0 25 0 1 0 487481532 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.07
CPU time (s): 1200.09
CPU user time (s): 1199.46
CPU system time (s): 0.635903
CPU usage (%): 100.002
Max. virtual memory (Kb): 83508
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####