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-ii8a4.opb
MD5SUM	8a77190c2eeefb9e88447a9087adfd6f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	283
Optimality of the best value was proved	NO
Number of terms in the objective function	792
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	792
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	792
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.02084
Number of variables	792
Total number of constraints	3194
Number of constraints which are clauses	3194
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	8
Trace number 4918

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-13 20:50:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=1490 boxname=wulflinc19 idbench=166 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  8a77190c2eeefb9e88447a9087adfd6f  /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc19/normalized-ii8a4.opb
IDLAUNCH: 1490
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        893696 kB
Buffers:         33424 kB
Cached:          74028 kB
SwapCached:         56 kB
Active:          45160 kB
Inactive:        65256 kB
HighTotal:      131008 kB
HighFree:        53004 kB
LowTotal:       903652 kB
LowFree:        840692 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            24984 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:10:23 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 1490 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3194 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 |    3194     8388 |    1064       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 354[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:36470     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   47626   112246 |   15875       4       26     6.5 |  0.000 % |
c |       104 |   47361   111687 |   17462      93     1225    13.2 |  0.521 % |
c |       254 |   47361   111687 |   19208     243     4630    19.1 |  0.521 % |
c ==============================================================================
c [1mFound solution: 346[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       431 |   47442   111960 |   15814     419     7912    18.9 |  0.521 % |
c |       533 |   47360   111784 |   17395     519    11037    21.3 |  0.777 % |
c ==============================================================================
c [1mFound solution: 319[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       582 |   47671   112647 |   15890     567    12211    21.5 |  0.777 % |
c |       682 |   47671   112647 |   17479     667    13724    20.6 |  0.860 % |
c |       834 |   47671   112647 |   19226     819    15865    19.4 |  0.860 % |
c |      1060 |   47629   112553 |   21149    1044    23666    22.7 |  0.945 % |
c |      1397 |   46908   110974 |   23264    1363    35493    26.0 |  2.354 % |
c |      1903 |   46287   109586 |   25591    1851    65230    35.2 |  3.588 % |
c ==============================================================================
c [1mFound solution: 294[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2040 |   46486   110113 |   15495    1975    65744    33.3 |  3.588 % |
c |      2141 |   46486   110113 |   17044    2076    68018    32.8 |  3.771 % |
c |      2292 |   46486   110113 |   18748    2227    72609    32.6 |  3.771 % |
c |      2518 |   46433   109991 |   20623    2452    84110    34.3 |  3.882 % |
c |      2857 |   46312   109724 |   22686    2785   100451    36.1 |  4.120 % |
c |      3365 |   46312   109724 |   24954    3293   114048    34.6 |  4.120 % |
c ==============================================================================
c [1mFound solution: 283[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3625 |   46434   110062 |   15478    3553   118845    33.4 |  4.120 % |
c |      3725 |   46354   109900 |   17025    3649   124499    34.1 |  4.296 % |
c |      3875 |   46354   109900 |   18728    3799   129147    34.0 |  4.296 % |
c |      4100 |   46264   109704 |   20601    4022   140449    34.9 |  4.469 % |
c |      4437 |   45953   109018 |   22661    4287   150386    35.1 |  5.077 % |
c |      4943 |   45894   108887 |   24927    4792   219227    45.7 |  5.194 % |
c |      5702 |   45382   107757 |   27420    5532   256414    46.4 |  6.189 % |
c |      6841 |   45339   107666 |   30162    6668   364309    54.6 |  6.267 % |
c |      8549 |   45288   107557 |   33178    8373   491019    58.6 |  6.362 % |
c |     11112 |   45168   107273 |   36496   10923   611414    56.0 |  6.622 % |
c |     14956 |   45122   107167 |   40145   14759   795096    53.9 |  6.719 % |
c |     20724 |   45026   106949 |   44160   20508  1308058    63.8 |  6.918 % |
c |     29373 |   45026   106949 |   48576   29157  2150568    73.8 |  6.918 % |
c |     42347 |   45026   106949 |   53434   42131  2922952    69.4 |  6.918 % |
c |     61808 |   45000   106891 |   58777   21517  1280796    59.5 |  6.970 % |
c |     91000 |   44991   106872 |   64655   50708  3380801    66.7 |  6.986 % |
c |    134789 |   44882   106619 |   71120   46306  3138339    67.8 |  7.220 % |
c |    200473 |   44882   106619 |   78233   57666  3417826    59.3 |  7.220 % |
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#### 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.91 0.95 0.90 2/55 25760
Raw data (stat): 25760 (runsolver) R 25759 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478958823 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/55 25760
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 2817 0 0 0 992 6 0 0 25 0 1 0 478958823 13676544 2742 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3339 2742 603 41 0 3298 0
vsize: 13356
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 25760
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3088 0 0 0 1991 7 0 0 25 0 1 0 478958823 14884864 3013 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3634 3013 603 41 0 3593 0
vsize: 14536
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25760
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3354 0 0 0 2989 8 0 0 25 0 1 0 478958823 16003072 3279 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3907 3279 603 41 0 3866 0
vsize: 15628
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25760
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3595 0 0 0 3988 9 0 0 25 0 1 0 478958823 16936960 3520 4294967295 134512640 134672761 3221224640 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4135 3520 603 41 0 4094 0
vsize: 16540
[startup+50.0026 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 25760
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 3870 0 0 0 4988 10 0 0 25 0 1 0 478958823 18141184 3795 4294967295 134512640 134672761 3221224640 3221223596 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4429 3795 603 41 0 4388 0
vsize: 17716
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4147 0 0 0 5987 11 0 0 25 0 1 0 478958823 19210240 4072 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4072 603 41 0 4649 0
vsize: 18760
[startup+70.0035 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4526 0 0 0 6986 12 0 0 25 0 1 0 478958823 20819968 4451 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5083 4451 603 41 0 5042 0
vsize: 20332
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 4798 0 0 0 7986 13 0 0 25 0 1 0 478958823 21880832 4723 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5342 4723 603 41 0 5301 0
vsize: 21368
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5057 0 0 0 8985 13 0 0 25 0 1 0 478958823 22929408 4982 4294967295 134512640 134672761 3221224640 3221223824 134559514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5598 4982 603 41 0 5557 0
vsize: 22392
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5288 0 0 0 9985 14 0 0 25 0 1 0 478958823 23859200 5213 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5825 5213 603 41 0 5784 0
vsize: 23300
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5494 0 0 0 10985 14 0 0 25 0 1 0 478958823 24776704 5419 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6049 5419 603 41 0 6008 0
vsize: 24196
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5686 0 0 0 11984 15 0 0 25 0 1 0 478958823 25575424 5611 4294967295 134512640 134672761 3221224640 3221223824 134559199 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6244 5611 603 41 0 6203 0
vsize: 24976
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 5859 0 0 0 12983 16 0 0 25 0 1 0 478958823 26247168 5784 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6408 5784 603 41 0 6367 0
vsize: 25632
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6066 0 0 0 13983 16 0 0 25 0 1 0 478958823 27185152 5991 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6637 5991 603 41 0 6596 0
vsize: 26548
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6285 0 0 0 14983 17 0 0 25 0 1 0 478958823 27983872 6210 4294967295 134512640 134672761 3221224640 3221223744 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6832 6210 603 41 0 6791 0
vsize: 27328
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6463 0 0 0 15982 18 0 0 25 0 1 0 478958823 28774400 6388 4294967295 134512640 134672761 3221224640 3221223744 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7025 6388 603 41 0 6984 0
vsize: 28100
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6646 0 0 0 16982 18 0 0 25 0 1 0 478958823 29446144 6571 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7189 6571 603 41 0 7148 0
vsize: 28756
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 6862 0 0 0 17982 18 0 0 25 0 1 0 478958823 30375936 6787 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7416 6787 603 41 0 7375 0
vsize: 29664
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7057 0 0 0 18981 19 0 0 25 0 1 0 478958823 31174656 6982 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7611 6982 603 41 0 7570 0
vsize: 30444
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7264 0 0 0 19981 20 0 0 25 0 1 0 478958823 31965184 7189 4294967295 134512640 134672761 3221224640 3221223700 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7804 7189 603 41 0 7763 0
vsize: 31216
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7449 0 0 0 20981 20 0 0 25 0 1 0 478958823 32763904 7374 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7999 7374 603 41 0 7958 0
vsize: 31996
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7608 0 0 0 21980 20 0 0 25 0 1 0 478958823 33419264 7533 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8159 7533 603 41 0 8118 0
vsize: 32636
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7758 0 0 0 22980 21 0 0 25 0 1 0 478958823 34074624 7683 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7683 603 41 0 8278 0
vsize: 33276
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 23980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7685 603 41 0 8278 0
vsize: 33276
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 24980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7685 603 41 0 8278 0
vsize: 33276
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 25980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7685 603 41 0 8278 0
vsize: 33276
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7760 0 0 0 26980 21 0 0 25 0 1 0 478958823 34074624 7685 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7685 603 41 0 8278 0
vsize: 33276
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7765 0 0 0 27981 21 0 0 25 0 1 0 478958823 34074624 7690 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7690 603 41 0 8278 0
vsize: 33276
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7766 0 0 0 28981 21 0 0 25 0 1 0 478958823 34074624 7691 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7691 603 41 0 8278 0
vsize: 33276
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7767 0 0 0 29981 21 0 0 25 0 1 0 478958823 34074624 7692 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7692 603 41 0 8278 0
vsize: 33276
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7767 0 0 0 30981 21 0 0 25 0 1 0 478958823 34074624 7692 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7692 603 41 0 8278 0
vsize: 33276
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7772 0 0 0 31981 21 0 0 25 0 1 0 478958823 34074624 7697 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7697 603 41 0 8278 0
vsize: 33276
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7773 0 0 0 32981 21 0 0 25 0 1 0 478958823 34074624 7698 4294967295 134512640 134672761 3221224640 3221223744 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7698 603 41 0 8278 0
vsize: 33276
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7779 0 0 0 33981 21 0 0 25 0 1 0 478958823 34074624 7704 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7704 603 41 0 8278 0
vsize: 33276
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25762
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7780 0 0 0 34982 21 0 0 25 0 1 0 478958823 34074624 7705 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8319 7705 603 41 0 8278 0
vsize: 33276
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7786 0 0 0 35982 21 0 0 25 0 1 0 478958823 34213888 7711 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8353 7711 603 41 0 8312 0
vsize: 33412
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7786 0 0 0 36981 21 0 0 25 0 1 0 478958823 34213888 7711 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8353 7711 603 41 0 8312 0
vsize: 33412
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7805 0 0 0 37981 22 0 0 25 0 1 0 478958823 34213888 7730 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8353 7730 603 41 0 8312 0
vsize: 33412
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7817 0 0 0 38982 22 0 0 25 0 1 0 478958823 34377728 7742 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7742 603 41 0 8352 0
vsize: 33572
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7818 0 0 0 39982 22 0 0 25 0 1 0 478958823 34377728 7743 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7743 603 41 0 8352 0
vsize: 33572
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7818 0 0 0 40982 22 0 0 25 0 1 0 478958823 34377728 7743 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7743 603 41 0 8352 0
vsize: 33572
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7819 0 0 0 41982 22 0 0 25 0 1 0 478958823 34377728 7744 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7744 603 41 0 8352 0
vsize: 33572
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7822 0 0 0 42982 22 0 0 25 0 1 0 478958823 34377728 7747 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8393 7747 603 41 0 8352 0
vsize: 33572
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 7953 0 0 0 43982 22 0 0 25 0 1 0 478958823 34906112 7878 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8522 7878 603 41 0 8481 0
vsize: 34088
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8101 0 0 0 44982 23 0 0 25 0 1 0 478958823 35438592 8026 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8652 8026 603 41 0 8611 0
vsize: 34608
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8243 0 0 0 45982 23 0 0 25 0 1 0 478958823 36233216 8168 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8846 8168 603 41 0 8805 0
vsize: 35384
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8377 0 0 0 46981 24 0 0 25 0 1 0 478958823 36888576 8302 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9006 8302 603 41 0 8965 0
vsize: 36024
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8467 0 0 0 47981 24 0 0 25 0 1 0 478958823 37158912 8392 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9072 8392 603 41 0 9031 0
vsize: 36288
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8467 0 0 0 48981 24 0 0 25 0 1 0 478958823 37158912 8392 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9072 8392 603 41 0 9031 0
vsize: 36288
[startup+500.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8477 0 0 0 49981 24 0 0 25 0 1 0 478958823 37318656 8402 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8402 603 41 0 9070 0
vsize: 36444
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8478 0 0 0 50981 24 0 0 25 0 1 0 478958823 37318656 8403 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8403 603 41 0 9070 0
vsize: 36444
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8478 0 0 0 51982 24 0 0 25 0 1 0 478958823 37318656 8403 4294967295 134512640 134672761 3221224640 3221223792 134541817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8403 603 41 0 9070 0
vsize: 36444
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 52982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8404 603 41 0 9070 0
vsize: 36444
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 53982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8404 603 41 0 9070 0
vsize: 36444
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8479 0 0 0 54982 24 0 0 25 0 1 0 478958823 37318656 8404 4294967295 134512640 134672761 3221224640 3221223824 134559291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8404 603 41 0 9070 0
vsize: 36444
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8485 0 0 0 55982 24 0 0 25 0 1 0 478958823 37318656 8410 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8410 603 41 0 9070 0
vsize: 36444
[startup+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 56982 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8411 603 41 0 9070 0
vsize: 36444
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25764
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 57985 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8411 603 41 0 9070 0
vsize: 36444
[startup+590.037 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8486 0 0 0 58984 24 0 0 25 0 1 0 478958823 37318656 8411 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8411 603 41 0 9070 0
vsize: 36444
[startup+600.037 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8487 0 0 0 59985 24 0 0 25 0 1 0 478958823 37318656 8412 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8412 603 41 0 9070 0
vsize: 36444
[startup+610.037 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8492 0 0 0 60984 25 0 0 25 0 1 0 478958823 37318656 8417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9111 8417 603 41 0 9070 0
vsize: 36444
[startup+620.038 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8505 0 0 0 61984 25 0 0 25 0 1 0 478958823 37482496 8430 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8430 603 41 0 9110 0
vsize: 36604
[startup+630.037 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8516 0 0 0 62985 25 0 0 25 0 1 0 478958823 37482496 8441 4294967295 134512640 134672761 3221224640 3221223788 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8441 603 41 0 9110 0
vsize: 36604
[startup+640.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8519 0 0 0 63985 25 0 0 25 0 1 0 478958823 37482496 8444 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8444 603 41 0 9110 0
vsize: 36604
[startup+650.038 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25817
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8521 0 0 0 64985 25 0 0 25 0 1 0 478958823 37482496 8446 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8446 603 41 0 9110 0
vsize: 36604
[startup+660.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8521 0 0 0 65985 25 0 0 25 0 1 0 478958823 37482496 8446 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8446 603 41 0 9110 0
vsize: 36604
[startup+670.038 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8522 0 0 0 66985 25 0 0 25 0 1 0 478958823 37482496 8447 4294967295 134512640 134672761 3221224640 3221223808 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8447 603 41 0 9110 0
vsize: 36604
[startup+680.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8523 0 0 0 67985 25 0 0 25 0 1 0 478958823 37482496 8448 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8448 603 41 0 9110 0
vsize: 36604
[startup+690.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8524 0 0 0 68986 25 0 0 25 0 1 0 478958823 37482496 8449 4294967295 134512640 134672761 3221224640 3221223824 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9151 8449 603 41 0 9110 0
vsize: 36604
[startup+700.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8552 0 0 0 69986 25 0 0 25 0 1 0 478958823 37679104 8477 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9199 8477 603 41 0 9158 0
vsize: 36796
[startup+710.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8562 0 0 0 70986 25 0 0 25 0 1 0 478958823 37871616 8487 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9246 8487 603 41 0 9205 0
vsize: 36984
[startup+720.039 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8565 0 0 0 71986 25 0 0 25 0 1 0 478958823 37871616 8490 4294967295 134512640 134672761 3221224640 3221223744 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9246 8490 603 41 0 9205 0
vsize: 36984
[startup+730.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8593 0 0 0 72986 25 0 0 25 0 1 0 478958823 37871616 8518 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9246 8518 603 41 0 9205 0
vsize: 36984
[startup+740.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8600 0 0 0 73986 25 0 0 25 0 1 0 478958823 38068224 8525 4294967295 134512640 134672761 3221224640 3221223824 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9294 8525 603 41 0 9253 0
vsize: 37176
[startup+750.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8709 0 0 0 74986 25 0 0 25 0 1 0 478958823 38461440 8634 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8634 603 41 0 9349 0
vsize: 37560
[startup+760.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8837 0 0 0 75986 26 0 0 25 0 1 0 478958823 38989824 8762 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9519 8762 603 41 0 9478 0
vsize: 38076
[startup+770.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 8955 0 0 0 76985 27 0 0 25 0 1 0 478958823 39391232 8880 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9617 8880 603 41 0 9576 0
vsize: 38468
[startup+780.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9075 0 0 0 77985 27 0 0 25 0 1 0 478958823 39919616 9000 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9746 9000 603 41 0 9705 0
vsize: 38984
[startup+790.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 78985 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223744 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9063 603 41 0 9769 0
vsize: 39240
[startup+800.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 79986 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223824 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9063 603 41 0 9769 0
vsize: 39240
[startup+810.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9138 0 0 0 80986 27 0 0 25 0 1 0 478958823 40181760 9063 4294967295 134512640 134672761 3221224640 3221223744 134560171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9063 603 41 0 9769 0
vsize: 39240
[startup+820.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9141 0 0 0 81986 27 0 0 25 0 1 0 478958823 40181760 9066 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9066 603 41 0 9769 0
vsize: 39240
[startup+830.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9149 0 0 0 82986 27 0 0 25 0 1 0 478958823 40181760 9074 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9074 603 41 0 9769 0
vsize: 39240
[startup+840.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9150 0 0 0 83986 27 0 0 25 0 1 0 478958823 40181760 9075 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9075 603 41 0 9769 0
vsize: 39240
[startup+850.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 84986 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223736 1075347241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9076 603 41 0 9769 0
vsize: 39240
[startup+860.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 85987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9076 603 41 0 9769 0
vsize: 39240
[startup+870.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 86987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9076 603 41 0 9769 0
vsize: 39240
[startup+880.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9151 0 0 0 87987 27 0 0 25 0 1 0 478958823 40181760 9076 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9076 603 41 0 9769 0
vsize: 39240
[startup+890.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25821
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9152 0 0 0 88987 27 0 0 25 0 1 0 478958823 40181760 9077 4294967295 134512640 134672761 3221224640 3221223808 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9077 603 41 0 9769 0
vsize: 39240
[startup+900.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9152 0 0 0 89987 28 0 0 25 0 1 0 478958823 40181760 9077 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9810 9077 603 41 0 9769 0
vsize: 39240
[startup+910.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9157 0 0 0 90987 28 0 0 25 0 1 0 478958823 40316928 9082 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9082 603 41 0 9802 0
vsize: 39372
[startup+920.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9158 0 0 0 91987 28 0 0 25 0 1 0 478958823 40316928 9083 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9083 603 41 0 9802 0
vsize: 39372
[startup+930.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9159 0 0 0 92987 28 0 0 25 0 1 0 478958823 40316928 9084 4294967295 134512640 134672761 3221224640 3221223744 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9084 603 41 0 9802 0
vsize: 39372
[startup+940.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9169 0 0 0 93988 28 0 0 25 0 1 0 478958823 40316928 9094 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9094 603 41 0 9802 0
vsize: 39372
[startup+950.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25823
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 94988 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223744 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9095 603 41 0 9802 0
vsize: 39372
[startup+960.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 95988 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9095 603 41 0 9802 0
vsize: 39372
[startup+970.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 96987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223744 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9843 9095 603 41 0 9802 0
vsize: 39372
[startup+980.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 97987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9095 603 41 0 9802 0
vsize: 39372
[startup+990.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9170 0 0 0 98987 28 0 0 25 0 1 0 478958823 40316928 9095 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9843 9095 603 41 0 9802 0
vsize: 39372
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9194 0 0 0 99987 28 0 0 25 0 1 0 478958823 40513536 9119 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9119 603 41 0 9850 0
vsize: 39564
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9196 0 0 0 100987 28 0 0 25 0 1 0 478958823 40513536 9121 4294967295 134512640 134672761 3221224640 3221223800 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9121 603 41 0 9850 0
vsize: 39564
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 101988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9122 603 41 0 9850 0
vsize: 39564
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 102988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9122 603 41 0 9850 0
vsize: 39564
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9197 0 0 0 103988 28 0 0 25 0 1 0 478958823 40513536 9122 4294967295 134512640 134672761 3221224640 3221223744 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9122 603 41 0 9850 0
vsize: 39564
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9198 0 0 0 104988 28 0 0 25 0 1 0 478958823 40513536 9123 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9123 603 41 0 9850 0
vsize: 39564
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9198 0 0 0 105988 28 0 0 25 0 1 0 478958823 40513536 9123 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9123 603 41 0 9850 0
vsize: 39564
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9199 0 0 0 106988 29 0 0 25 0 1 0 478958823 40513536 9124 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9124 603 41 0 9850 0
vsize: 39564
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9201 0 0 0 107989 29 0 0 25 0 1 0 478958823 40513536 9126 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9126 603 41 0 9850 0
vsize: 39564
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9203 0 0 0 108989 29 0 0 25 0 1 0 478958823 40513536 9128 4294967295 134512640 134672761 3221224640 3221223824 134558848 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9128 603 41 0 9850 0
vsize: 39564
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 109989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 110989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 111989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223744 134560198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 112989 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 113990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 114990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 115990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1170.05 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 116990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1180.05 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9206 0 0 0 117990 29 0 0 25 0 1 0 478958823 40513536 9131 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9131 603 41 0 9850 0
vsize: 39564
[startup+1190.06 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9209 0 0 0 118991 29 0 0 25 0 1 0 478958823 40513536 9134 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9134 603 41 0 9850 0
vsize: 39564
[startup+1200.06 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 25825
Raw data (stat): 25760 (minisat+) R 25759 22929 22928 0 -1 0 9209 0 0 0 119991 29 0 0 25 0 1 0 478958823 40513536 9134 4294967295 134512640 134672761 3221224640 3221223744 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9891 9134 603 41 0 9850 0
vsize: 39564
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.04 1.00 0.92 1/55 25825
Raw data (stat): 25760 (minisat+) Z 25759 22929 22928 0 -1 12 9212 0 0 0 119991 31 0 0 25 0 1 0 478958823 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.08
CPU time (s): 1200.23
CPU user time (s): 1199.92
CPU system time (s): 0.311952
CPU usage (%): 100.012
Max. virtual memory (Kb): 39564
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####