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/manquinho/primes-dimacs-cnf/normalized-ii8c1.opb
MD5SUM	5573ac468e70af6b65c69997b62e5033
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	302
Optimality of the best value was proved	NO
Number of terms in the objective function	1020
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	1020
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1020
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02984
Number of variables	1020
Total number of constraints	3575
Number of constraints which are clauses	3575
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	10
Trace number 4927

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        920808 kB
Buffers:         34660 kB
Cached:          60048 kB
SwapCached:         16 kB
Active:          58924 kB
Inactive:        38644 kB
HighTotal:      131008 kB
HighFree:        67088 kB
LowTotal:       903652 kB
LowFree:        853720 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10736 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:11:51 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 1535 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3575 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 |    3575     8330 |    1191       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 315[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:47988     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   60591   141413 |   20197       0        0     nan |  0.000 % |
c |       100 |   59847   139829 |   22216      80     1790    22.4 |  1.091 % |
c |       250 |   59683   139471 |   24438     226     5037    22.3 |  1.342 % |
c |       476 |   59275   138571 |   26882     444    24386    54.9 |  1.980 % |
c |       814 |   58464   136786 |   29570     764    31843    41.7 |  3.241 % |
c |      1322 |   57828   135368 |   32527    1250    44363    35.5 |  4.255 % |
c |      2081 |   57828   135368 |   35780    2009    72239    36.0 |  4.255 % |
c |      3223 |   57063   133687 |   39358    3019   107276    35.5 |  5.441 % |
c |      4931 |   56757   133033 |   43294    4721   159290    33.7 |  5.892 % |
c |      7493 |   56757   133033 |   47623    7283   284105    39.0 |  5.892 % |
c |     11337 |   56149   131689 |   52385   11111   781407    70.3 |  6.846 % |
c |     17103 |   56082   131532 |   57624   16867  1524305    90.4 |  6.962 % |
c |     25753 |   56082   131532 |   63386   25517  2983991   116.9 |  6.962 % |
c |     38727 |   56043   131433 |   69725   38475  4273840   111.1 |  7.040 % |
c |     58188 |   56043   131433 |   76698   57936  6608517   114.1 |  7.040 % |
c |     87381 |   56043   131433 |   84367   21372  1717107    80.3 |  7.040 % |
c |    131170 |   55952   131220 |   92804   65147  7208888   110.7 |  7.198 % |
c |    196855 |   55952   131220 |  102085   48595  4741331    97.6 |  7.198 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -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 -x737 -x738 -x739 #### 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.90 0.95 0.90 2/54 28017
Raw data (stat): 28017 (runsolver) R 28016 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420747944 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0008 s]
Raw data (loadavg): 0.92 0.95 0.90 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 3536 0 0 0 988 9 0 0 25 0 1 0 420747944 17215488 3363 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4203 3363 603 41 0 4162 0
vsize: 16812
[startup+20.0014 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 3847 0 0 0 1987 10 0 0 25 0 1 0 420747944 18452480 3674 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4505 3674 603 41 0 4464 0
vsize: 18020
[startup+30.0028 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 4427 0 0 0 2984 12 0 0 25 0 1 0 420747944 20742144 4254 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5064 4254 603 41 0 5023 0
vsize: 20256
[startup+40.0031 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 4791 0 0 0 3982 14 0 0 25 0 1 0 420747944 22216704 4618 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5424 4618 603 41 0 5383 0
vsize: 21696
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 5238 0 0 0 4980 15 0 0 25 0 1 0 420747944 24109056 5065 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5886 5065 603 41 0 5845 0
vsize: 23544
[startup+60.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 5641 0 0 0 5979 17 0 0 25 0 1 0 420747944 25845760 5468 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6310 5468 603 41 0 6269 0
vsize: 25240
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 6064 0 0 0 6978 18 0 0 25 0 1 0 420747944 27578368 5891 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6733 5891 603 41 0 6692 0
vsize: 26932
[startup+80.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 6475 0 0 0 7977 19 0 0 25 0 1 0 420747944 29179904 6302 4294967295 134512640 134672761 3221224640 3221223744 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7124 6302 603 41 0 7083 0
vsize: 28496
[startup+90.0035 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 6768 0 0 0 8976 20 0 0 25 0 1 0 420747944 30388224 6595 4294967295 134512640 134672761 3221224640 3221223824 134558678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7419 6595 603 41 0 7378 0
vsize: 29676
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 7154 0 0 0 9976 21 0 0 25 0 1 0 420747944 31997952 6981 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7812 6981 603 41 0 7771 0
vsize: 31248
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 7517 0 0 0 10975 22 0 0 25 0 1 0 420747944 33599488 7344 4294967295 134512640 134672761 3221224640 3221223808 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8203 7344 603 41 0 8162 0
vsize: 32812
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 7762 0 0 0 11974 23 0 0 25 0 1 0 420747944 34545664 7589 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8434 7589 603 41 0 8393 0
vsize: 33736
[startup+130.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 8007 0 0 0 12973 24 0 0 25 0 1 0 420747944 35618816 7834 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8696 7834 603 41 0 8655 0
vsize: 34784
[startup+140.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 8241 0 0 0 13972 25 0 0 25 0 1 0 420747944 36556800 8068 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8925 8068 603 41 0 8884 0
vsize: 35700
[startup+150.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 8523 0 0 0 14970 26 0 0 25 0 1 0 420747944 37621760 8350 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9185 8350 603 41 0 9144 0
vsize: 36740
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 8823 0 0 0 15969 27 0 0 25 0 1 0 420747944 38825984 8650 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9479 8650 603 41 0 9438 0
vsize: 37916
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 9123 0 0 0 16969 28 0 0 25 0 1 0 420747944 40157184 8950 4294967295 134512640 134672761 3221224640 3221223744 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9804 8950 603 41 0 9763 0
vsize: 39216
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 9422 0 0 0 17968 29 0 0 25 0 1 0 420747944 41357312 9249 4294967295 134512640 134672761 3221224640 3221223744 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10097 9249 603 41 0 10056 0
vsize: 40388
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 9704 0 0 0 18967 30 0 0 25 0 1 0 420747944 42426368 9531 4294967295 134512640 134672761 3221224640 3221223808 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10358 9531 603 41 0 10317 0
vsize: 41432
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 10021 0 0 0 19966 31 0 0 25 0 1 0 420747944 43765760 9848 4294967295 134512640 134672761 3221224640 3221223744 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10685 9848 603 41 0 10644 0
vsize: 42740
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 10356 0 0 0 20965 32 0 0 25 0 1 0 420747944 45088768 10183 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11008 10183 603 41 0 10967 0
vsize: 44032
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 10617 0 0 0 21965 32 0 0 25 0 1 0 420747944 46145536 10444 4294967295 134512640 134672761 3221224640 3221223808 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11266 10444 603 41 0 11225 0
vsize: 45064
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 10807 0 0 0 22965 33 0 0 25 0 1 0 420747944 46944256 10634 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11461 10635 603 41 0 11420 0
vsize: 45844
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 11044 0 0 0 23963 34 0 0 25 0 1 0 420747944 47874048 10871 4294967295 134512640 134672761 3221224640 3221223824 134558656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11688 10871 603 41 0 11647 0
vsize: 46752
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 11242 0 0 0 24963 34 0 0 25 0 1 0 420747944 48676864 11069 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11884 11069 603 41 0 11843 0
vsize: 47536
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 11415 0 0 0 25963 35 0 0 25 0 1 0 420747944 49737728 11242 4294967295 134512640 134672761 3221224640 3221223744 134559941 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12143 11242 603 41 0 12102 0
vsize: 48572
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 11626 0 0 0 26962 36 0 0 25 0 1 0 420747944 50536448 11453 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12338 11453 603 41 0 12297 0
vsize: 49352
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 11822 0 0 0 27962 37 0 0 25 0 1 0 420747944 51335168 11649 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12533 11649 603 41 0 12492 0
vsize: 50132
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12004 0 0 0 28961 38 0 0 25 0 1 0 420747944 52129792 11831 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11831 603 41 0 12686 0
vsize: 50908
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12197 0 0 0 29960 38 0 0 25 0 1 0 420747944 52797440 12024 4294967295 134512640 134672761 3221224640 3221223744 134560293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12890 12024 603 41 0 12849 0
vsize: 51560
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12393 0 0 0 30960 39 0 0 25 0 1 0 420747944 53587968 12220 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13083 12220 603 41 0 13042 0
vsize: 52332
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12588 0 0 0 31959 40 0 0 25 0 1 0 420747944 54378496 12415 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13276 12415 603 41 0 13235 0
vsize: 53104
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12763 0 0 0 32959 41 0 0 25 0 1 0 420747944 55169024 12590 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13469 12590 603 41 0 13428 0
vsize: 53876
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 12937 0 0 0 33959 41 0 0 25 0 1 0 420747944 55848960 12764 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13635 12764 603 41 0 13594 0
vsize: 54540
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13114 0 0 0 34958 41 0 0 25 0 1 0 420747944 56651776 12941 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13831 12941 603 41 0 13790 0
vsize: 55324
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13324 0 0 0 35958 42 0 0 25 0 1 0 420747944 57450496 13151 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14026 13151 603 41 0 13985 0
vsize: 56104
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 36958 42 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 37958 42 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 38957 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 39957 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 40957 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 41957 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223596 1075350251 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 42958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 43958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 44958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 45958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 46958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 47958 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28017
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 48959 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+500.034 s]
Raw data (loadavg): 0.99 0.97 0.91 3/58 28060
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 49961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+510.034 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 50961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+520.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 51961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+530.033 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 52961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+540.033 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 53961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+550.033 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 54961 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+560.034 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 55962 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+570.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28070
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 56962 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223804 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+580.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 57962 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+590.039 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 58963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+600.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 59963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+610.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 60963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+620.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 61963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223776 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+630.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 62963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223824 134559383 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+640.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 63963 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+650.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 64964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+660.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 65964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+670.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 66964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+680.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 67964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+690.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 68964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+700.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 69964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+710.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13497 0 0 0 70964 43 0 0 25 0 1 0 420747944 58105856 13324 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13324 603 41 0 14145 0
vsize: 56744
[startup+720.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13507 0 0 0 71964 43 0 0 25 0 1 0 420747944 58286080 13334 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13334 603 41 0 14189 0
vsize: 56920
[startup+730.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13507 0 0 0 72964 43 0 0 25 0 1 0 420747944 58286080 13334 4294967295 134512640 134672761 3221224640 3221223824 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13334 603 41 0 14189 0
vsize: 56920
[startup+740.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13519 0 0 0 73964 43 0 0 25 0 1 0 420747944 58286080 13346 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13346 603 41 0 14189 0
vsize: 56920
[startup+750.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13519 0 0 0 74965 43 0 0 25 0 1 0 420747944 58286080 13346 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13346 603 41 0 14189 0
vsize: 56920
[startup+760.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13519 0 0 0 75965 43 0 0 25 0 1 0 420747944 58286080 13346 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13346 603 41 0 14189 0
vsize: 56920
[startup+770.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13519 0 0 0 76965 43 0 0 25 0 1 0 420747944 58286080 13346 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13346 603 41 0 14189 0
vsize: 56920
[startup+780.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13519 0 0 0 77965 43 0 0 25 0 1 0 420747944 58286080 13346 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13346 603 41 0 14189 0
vsize: 56920
[startup+790.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13531 0 0 0 78965 43 0 0 25 0 1 0 420747944 58286080 13358 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13358 603 41 0 14189 0
vsize: 56920
[startup+800.042 s]
Raw data (loadavg): 1.00 0.99 0.91 3/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13533 0 0 0 79966 43 0 0 25 0 1 0 420747944 58286080 13360 4294967295 134512640 134672761 3221224640 3221223872 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13360 603 41 0 14189 0
vsize: 56920
[startup+810.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13534 0 0 0 80966 43 0 0 25 0 1 0 420747944 58286080 13361 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14230 13361 603 41 0 14189 0
vsize: 56920
[startup+820.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13655 0 0 0 81965 43 0 0 25 0 1 0 420747944 58810368 13482 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14358 13482 603 41 0 14317 0
vsize: 57432
[startup+830.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28072
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13799 0 0 0 82965 44 0 0 25 0 1 0 420747944 59473920 13626 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14520 13626 603 41 0 14479 0
vsize: 58080
[startup+840.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 13934 0 0 0 83965 44 0 0 25 0 1 0 420747944 59998208 13761 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14648 13761 603 41 0 14607 0
vsize: 58592
[startup+850.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14070 0 0 0 84965 44 0 0 25 0 1 0 420747944 60530688 13897 4294967295 134512640 134672761 3221224640 3221223792 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14778 13897 603 41 0 14737 0
vsize: 59112
[startup+860.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14195 0 0 0 85965 45 0 0 25 0 1 0 420747944 61067264 14022 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14909 14022 603 41 0 14868 0
vsize: 59636
[startup+870.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14341 0 0 0 86965 45 0 0 25 0 1 0 420747944 61595648 14168 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15038 14168 603 41 0 14997 0
vsize: 60152
[startup+880.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14480 0 0 0 87964 46 0 0 25 0 1 0 420747944 62255104 14307 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14307 603 41 0 15158 0
vsize: 60796
[startup+890.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14613 0 0 0 88964 46 0 0 25 0 1 0 420747944 62779392 14440 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15327 14440 603 41 0 15286 0
vsize: 61308
[startup+900.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14726 0 0 0 89964 47 0 0 25 0 1 0 420747944 63172608 14553 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15423 14553 603 41 0 15382 0
vsize: 61692
[startup+910.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14854 0 0 0 90963 47 0 0 25 0 1 0 420747944 63766528 14681 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15568 14681 603 41 0 15527 0
vsize: 62272
[startup+920.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 14975 0 0 0 91963 48 0 0 25 0 1 0 420747944 64290816 14802 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15696 14802 603 41 0 15655 0
vsize: 62784
[startup+930.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15073 0 0 0 92962 48 0 0 25 0 1 0 420747944 64688128 14900 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15793 14900 603 41 0 15752 0
vsize: 63172
[startup+940.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15194 0 0 0 93962 49 0 0 25 0 1 0 420747944 65282048 15021 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15938 15021 603 41 0 15897 0
vsize: 63752
[startup+950.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15331 0 0 0 94962 49 0 0 25 0 1 0 420747944 65818624 15158 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16069 15158 603 41 0 16028 0
vsize: 64276
[startup+960.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15479 0 0 0 95962 50 0 0 25 0 1 0 420747944 66478080 15306 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16230 15306 603 41 0 16189 0
vsize: 64920
[startup+970.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15633 0 0 0 96961 50 0 0 25 0 1 0 420747944 67002368 15460 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16358 15460 603 41 0 16317 0
vsize: 65432
[startup+980.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15766 0 0 0 97961 51 0 0 25 0 1 0 420747944 67661824 15593 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16519 15593 603 41 0 16478 0
vsize: 66076
[startup+990.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 15903 0 0 0 98961 51 0 0 25 0 1 0 420747944 68198400 15730 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16650 15730 603 41 0 16609 0
vsize: 66600
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16052 0 0 0 99961 52 0 0 25 0 1 0 420747944 68726784 15879 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16779 15879 603 41 0 16738 0
vsize: 67116
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 100960 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223296 134565777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 101961 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 102961 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 103961 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 104961 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 105961 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 106962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 107962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 108962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 109962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223744 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 110962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 111962 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 112963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 113963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 114963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 115963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 116963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 117963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 118964 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28074
Raw data (stat): 28017 (minisat+) R 28016 25285 25284 0 -1 0 16184 0 0 0 119963 52 0 0 25 0 1 0 420747944 69251072 16011 4294967295 134512640 134672761 3221224640 3221223744 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16907 16011 603 41 0 16866 0
vsize: 67628
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28074
Raw data (stat): 28017 (minisat+) Z 28016 25285 25284 0 -1 12 16187 0 0 0 119964 55 0 0 25 0 1 0 420747944 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.2
CPU user time (s): 1199.64
CPU system time (s): 0.555915
CPU usage (%): 100.009
Max. virtual memory (Kb): 67628
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####