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-ii8b2.opb
MD5SUM	bbfcebd70586668574286ad19a1cd5a8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	379
Optimality of the best value was proved	NO
Number of terms in the objective function	1152
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	1152
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1152
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03984
Number of variables	1152
Total number of constraints	4664
Number of constraints which are clauses	4664
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 4920

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        870116 kB
Buffers:         30992 kB
Cached:          90476 kB
SwapCached:        524 kB
Active:          42016 kB
Inactive:        82880 kB
HighTotal:      131008 kB
HighFree:        36708 kB
LowTotal:       903652 kB
LowFree:        833408 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34080 kB
Committed_AS:    63496 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:10:33 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 1508 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4664 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 |    4664    10368 |    1554       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 418[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63108     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |   80342   187277 |   26780       4       53    13.2 |  0.000 % |
c |       105 |   80295   187182 |   29458     103     4570    44.4 |  0.068 % |
c |       255 |   80295   187182 |   32403     253    11493    45.4 |  0.068 % |
c |       480 |   78340   182905 |   35644     415    22935    55.3 |  2.335 % |
c |       818 |   78287   182784 |   39208     750    30890    41.2 |  2.402 % |
c |      1325 |   78287   182784 |   43129    1257    74531    59.3 |  2.402 % |
c |      2085 |   78203   182602 |   47442    2015   104674    51.9 |  2.498 % |
c ==============================================================================
c [1mFound solution: 395[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 |      2395 |   78562   183587 |   26187    2325   119226    51.3 |  2.498 % |
c |      2496 |   78562   183587 |   28805    2426   120994    49.9 |  2.488 % |
c |      2646 |   78562   183587 |   31686    2576   125847    48.9 |  2.488 % |
c |      2871 |   78562   183587 |   34854    2801   133995    47.8 |  2.488 % |
c |      3208 |   78499   183450 |   38340    3137   143848    45.9 |  2.560 % |
c |      3716 |   77783   181858 |   42174    3570   162643    45.6 |  3.412 % |
c |      4476 |   77760   181811 |   46391    4139   190783    46.1 |  3.433 % |
c |      5616 |   77632   181541 |   51031    5272   314876    59.7 |  3.567 % |
c |      7324 |   77587   181446 |   56134    6979   364272    52.2 |  3.616 % |
c |      9888 |   77395   181025 |   61747    9516   439997    46.2 |  3.836 % |
c |     13733 |   77233   180675 |   67922   13357   771030    57.7 |  4.014 % |
c ==============================================================================
c [1mFound solution: 387[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 |     17494 |   77317   180956 |   25772   17111   909290    53.1 |  4.014 % |
c |     17594 |   77317   180956 |   28349   17211   912798    53.0 |  4.079 % |
c |     17745 |   77301   180922 |   31184   17359   917832    52.9 |  4.097 % |
c |     17971 |   77301   180922 |   34302   17585   922741    52.5 |  4.097 % |
c |     18308 |   77301   180922 |   37732   17922   975464    54.4 |  4.097 % |
c |     18814 |   77000   180271 |   41506   18420   993851    54.0 |  4.430 % |
c ==============================================================================
c [1mFound solution: 384[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 |     19542 |   76949   180180 |   25649   19073   997675    52.3 |  4.430 % |
c |     19642 |   76949   180180 |   28213   19173   999183    52.1 |  4.567 % |
c |     19792 |   76949   180180 |   31035   19323  1005573    52.0 |  4.567 % |
c |     20017 |   76865   179998 |   34138   19456  1010930    52.0 |  4.660 % |
c |     20354 |   76865   179998 |   37552   19793  1041428    52.6 |  4.660 % |
c |     20860 |   76865   179998 |   41307   20299  1059829    52.2 |  4.660 % |
c |     21619 |   76831   179926 |   45438   20274  1068528    52.7 |  4.697 % |
c |     22759 |   76831   179926 |   49982   21414  1107610    51.7 |  4.697 % |
c |     24468 |   76805   179864 |   54980   23097  1204602    52.2 |  4.732 % |
c |     27030 |   76805   179864 |   60479   25659  1423323    55.5 |  4.732 % |
c |     30876 |   76805   179864 |   66526   29505  1560456    52.9 |  4.732 % |
c |     36642 |   76805   179864 |   73179   35271  2075604    58.8 |  4.732 % |
c |     45292 |   76805   179864 |   80497   43921  2991534    68.1 |  4.732 % |
c ==============================================================================
c [1mFound solution: 380[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 |     57655 |   76754   179790 |   25584   55821  4052834    72.6 |  4.732 % |
c |     57755 |   76754   179790 |   28142   18665  1212846    65.0 |  4.881 % |
c |     57905 |   76754   179790 |   30956   18815  1221408    64.9 |  4.881 % |
c |     58132 |   76754   179790 |   34052   19042  1230212    64.6 |  4.881 % |
c |     58469 |   76691   179657 |   37457   19378  1238118    63.9 |  4.949 % |
c |     58975 |   76691   179657 |   41203   19884  1286725    64.7 |  4.949 % |
c |     59734 |   76637   179539 |   45323   20642  1347364    65.3 |  5.011 % |
c |     60874 |   76635   179535 |   49855   21781  1441910    66.2 |  5.013 % |
c |     62582 |   76635   179535 |   54841   23489  1579487    67.2 |  5.013 % |
c |     65147 |   76592   179438 |   60325   26053  1740507    66.8 |  5.063 % |
c |     68991 |   76592   179438 |   66358   29897  2141648    71.6 |  5.063 % |
c |     74758 |   76592   179438 |   72994   35664  2591073    72.7 |  5.063 % |
c |     83407 |   76592   179438 |   80293   44313  3254447    73.4 |  5.063 % |
c |     96381 |   76550   179348 |   88322   57274  4197372    73.3 |  5.108 % |
c |    115843 |   76550   179348 |   97155   76736  5614266    73.2 |  5.108 % |
c |    145036 |   76550   179348 |  106870  105929  7745460    73.1 |  5.108 % |
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#### 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/54 28512
Raw data (stat): 28512 (runsolver) R 28511 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478962674 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.001 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 4377 0 0 0 987 10 0 0 25 0 1 0 478962674 19681280 4173 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4805 4173 603 41 0 4764 0
vsize: 19220
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 4642 0 0 0 1986 11 0 0 25 0 1 0 478962674 21803008 4438 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5323 4438 603 41 0 5282 0
vsize: 21292
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 4826 0 0 0 2984 12 0 0 25 0 1 0 478962674 22589440 4622 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5515 4622 603 41 0 5474 0
vsize: 22060
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5092 0 0 0 3983 13 0 0 25 0 1 0 478962674 23650304 4888 4294967295 134512640 134672761 3221224640 3221223808 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5774 4888 603 41 0 5733 0
vsize: 23096
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5293 0 0 0 4983 14 0 0 25 0 1 0 478962674 24444928 5089 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5968 5089 603 41 0 5927 0
vsize: 23872
[startup+60.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5478 0 0 0 5983 15 0 0 25 0 1 0 478962674 25251840 5274 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6165 5274 603 41 0 6124 0
vsize: 24660
[startup+70.0019 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5613 0 0 0 6982 15 0 0 25 0 1 0 478962674 25825280 5409 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6305 5409 603 41 0 6264 0
vsize: 25220
[startup+80.0029 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5691 0 0 0 7982 16 0 0 25 0 1 0 478962674 26230784 5487 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6404 5487 603 41 0 6363 0
vsize: 25616
[startup+90.0026 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 5821 0 0 0 8981 16 0 0 25 0 1 0 478962674 26636288 5617 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6503 5617 603 41 0 6462 0
vsize: 26012
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6012 0 0 0 9981 17 0 0 25 0 1 0 478962674 27439104 5808 4294967295 134512640 134672761 3221224640 3221223808 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6699 5808 603 41 0 6658 0
vsize: 26796
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6170 0 0 0 10981 17 0 0 25 0 1 0 478962674 28106752 5966 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6862 5966 603 41 0 6821 0
vsize: 27448
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6326 0 0 0 11980 18 0 0 25 0 1 0 478962674 28782592 6122 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7027 6122 603 41 0 6986 0
vsize: 28108
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6512 0 0 0 12980 18 0 0 25 0 1 0 478962674 29454336 6308 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7191 6308 603 41 0 7150 0
vsize: 28764
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6708 0 0 0 13980 18 0 0 25 0 1 0 478962674 30371840 6504 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7415 6504 603 41 0 7374 0
vsize: 29660
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 6891 0 0 0 14980 19 0 0 25 0 1 0 478962674 31158272 6687 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7607 6687 603 41 0 7566 0
vsize: 30428
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7015 0 0 0 15979 20 0 0 25 0 1 0 478962674 31686656 6811 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7736 6811 603 41 0 7695 0
vsize: 30944
[startup+170.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7186 0 0 0 16979 20 0 0 25 0 1 0 478962674 32354304 6982 4294967295 134512640 134672761 3221224640 3221223744 134560520 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7899 6982 603 41 0 7858 0
vsize: 31596
[startup+180.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7358 0 0 0 17979 21 0 0 25 0 1 0 478962674 33021952 7154 4294967295 134512640 134672761 3221224640 3221223744 134559910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8062 7154 603 41 0 8021 0
vsize: 32248
[startup+190.005 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7548 0 0 0 18979 21 0 0 25 0 1 0 478962674 33812480 7344 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8255 7344 603 41 0 8214 0
vsize: 33020
[startup+200.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7718 0 0 0 19978 21 0 0 25 0 1 0 478962674 34476032 7514 4294967295 134512640 134672761 3221224640 3221223744 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8417 7514 603 41 0 8376 0
vsize: 33668
[startup+210.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 7864 0 0 0 20978 22 0 0 25 0 1 0 478962674 35155968 7660 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8583 7660 603 41 0 8542 0
vsize: 34332
[startup+220.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8013 0 0 0 21978 22 0 0 25 0 1 0 478962674 35680256 7809 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8711 7809 603 41 0 8670 0
vsize: 34844
[startup+230.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8162 0 0 0 22978 22 0 0 25 0 1 0 478962674 36347904 7958 4294967295 134512640 134672761 3221224640 3221223744 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8874 7958 603 41 0 8833 0
vsize: 35496
[startup+240.005 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8329 0 0 0 23977 23 0 0 25 0 1 0 478962674 36999168 8125 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9033 8125 603 41 0 8992 0
vsize: 36132
[startup+250.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8497 0 0 0 24977 24 0 0 25 0 1 0 478962674 37666816 8293 4294967295 134512640 134672761 3221224640 3221223776 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9196 8293 603 41 0 9155 0
vsize: 36784
[startup+260.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8663 0 0 0 25977 24 0 0 25 0 1 0 478962674 38326272 8459 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9357 8459 603 41 0 9316 0
vsize: 37428
[startup+270.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8817 0 0 0 26976 25 0 0 25 0 1 0 478962674 38985728 8613 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9518 8613 603 41 0 9477 0
vsize: 38072
[startup+280.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 8964 0 0 0 27976 25 0 0 25 0 1 0 478962674 39641088 8760 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9678 8760 603 41 0 9637 0
vsize: 38712
[startup+290.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 28975 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223904 134562492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+300.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 29975 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+310.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 30975 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+320.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 31976 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223788 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+330.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 32976 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+340.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 33976 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+350.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 34976 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+360.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 35977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223824 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+370.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 36977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+380.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 37977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223824 134559365 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+390.009 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 38977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+400.009 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 39977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+410.009 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 40977 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+420.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 41978 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+430.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 42978 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+440.009 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 43978 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+450.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 44978 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+460.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9113 0 0 0 45979 26 0 0 25 0 1 0 478962674 40140800 8909 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8909 603 41 0 9759 0
vsize: 39200
[startup+470.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 46979 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+480.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 47979 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+490.011 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 48979 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+500.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 49979 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223840 134557828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+510.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 50979 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+520.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 51980 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+530.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9114 0 0 0 52980 26 0 0 25 0 1 0 478962674 40140800 8910 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8910 603 41 0 9759 0
vsize: 39200
[startup+540.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9216 0 0 0 53980 26 0 0 25 0 1 0 478962674 40534016 9012 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9896 9012 603 41 0 9855 0
vsize: 39584
[startup+550.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9315 0 0 0 54979 27 0 0 25 0 1 0 478962674 41062400 9111 4294967295 134512640 134672761 3221224640 3221223744 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10025 9111 603 41 0 9984 0
vsize: 40100
[startup+560.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9408 0 0 0 55979 27 0 0 25 0 1 0 478962674 41320448 9204 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10088 9204 603 41 0 10047 0
vsize: 40352
[startup+570.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 28512
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9512 0 0 0 56979 27 0 0 25 0 1 0 478962674 41840640 9308 4294967295 134512640 134672761 3221224640 3221223776 134560640 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10215 9308 603 41 0 10174 0
vsize: 40860
[startup+580.012 s]
Raw data (loadavg): 1.15 1.03 0.93 3/58 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9614 0 0 0 57979 28 0 0 25 0 1 0 478962674 42258432 9410 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10317 9410 603 41 0 10276 0
vsize: 41268
[startup+590.012 s]
Raw data (loadavg): 1.13 1.03 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9697 0 0 0 58979 28 0 0 25 0 1 0 478962674 42520576 9493 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10381 9493 603 41 0 10340 0
vsize: 41524
[startup+600.012 s]
Raw data (loadavg): 1.11 1.03 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9779 0 0 0 59979 29 0 0 25 0 1 0 478962674 42917888 9575 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10478 9575 603 41 0 10437 0
vsize: 41912
[startup+610.012 s]
Raw data (loadavg): 1.09 1.03 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9874 0 0 0 60978 29 0 0 25 0 1 0 478962674 43311104 9670 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10574 9670 603 41 0 10533 0
vsize: 42296
[startup+620.012 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 9982 0 0 0 61978 29 0 0 25 0 1 0 478962674 43966464 9778 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10734 9778 603 41 0 10693 0
vsize: 42936
[startup+630.012 s]
Raw data (loadavg): 1.06 1.03 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10093 0 0 0 62978 30 0 0 25 0 1 0 478962674 44486656 9889 4294967295 134512640 134672761 3221224640 3221223776 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10861 9889 603 41 0 10820 0
vsize: 43444
[startup+640.012 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10180 0 0 0 63978 30 0 0 25 0 1 0 478962674 44752896 9976 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10926 9976 603 41 0 10885 0
vsize: 43704
[startup+650.013 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 28565
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10276 0 0 0 64978 30 0 0 25 0 1 0 478962674 45162496 10072 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11026 10072 603 41 0 10985 0
vsize: 44104
[startup+660.013 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10383 0 0 0 65978 30 0 0 25 0 1 0 478962674 45690880 10179 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11155 10179 603 41 0 11114 0
vsize: 44620
[startup+670.013 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10500 0 0 0 66978 30 0 0 25 0 1 0 478962674 46125056 10296 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11261 10296 603 41 0 11220 0
vsize: 45044
[startup+680.013 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10607 0 0 0 67978 30 0 0 25 0 1 0 478962674 46526464 10403 4294967295 134512640 134672761 3221224640 3221223744 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11359 10403 603 41 0 11318 0
vsize: 45436
[startup+690.013 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10709 0 0 0 68978 31 0 0 25 0 1 0 478962674 47050752 10505 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11487 10505 603 41 0 11446 0
vsize: 45948
[startup+700.014 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10825 0 0 0 69977 32 0 0 25 0 1 0 478962674 47448064 10621 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11584 10621 603 41 0 11543 0
vsize: 46336
[startup+710.014 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 10923 0 0 0 70978 32 0 0 25 0 1 0 478962674 47845376 10719 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11681 10719 603 41 0 11640 0
vsize: 46724
[startup+720.014 s]
Raw data (loadavg): 1.01 1.02 0.93 3/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11017 0 0 0 71977 32 0 0 25 0 1 0 478962674 48316416 10813 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11796 10813 603 41 0 11755 0
vsize: 47184
[startup+730.014 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11091 0 0 0 72977 32 0 0 25 0 1 0 478962674 48574464 10887 4294967295 134512640 134672761 3221224640 3221223744 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11859 10887 603 41 0 11818 0
vsize: 47436
[startup+740.013 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11219 0 0 0 73976 33 0 0 25 0 1 0 478962674 49098752 11015 4294967295 134512640 134672761 3221224640 3221223744 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11987 11015 603 41 0 11946 0
vsize: 47948
[startup+750.014 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11318 0 0 0 74976 33 0 0 25 0 1 0 478962674 49491968 11114 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11114 603 41 0 12042 0
vsize: 48332
[startup+760.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11413 0 0 0 75976 33 0 0 25 0 1 0 478962674 49885184 11209 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12179 11209 603 41 0 12138 0
vsize: 48716
[startup+770.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11513 0 0 0 76976 34 0 0 25 0 1 0 478962674 50278400 11309 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12275 11309 603 41 0 12234 0
vsize: 49100
[startup+780.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11614 0 0 0 77976 34 0 0 25 0 1 0 478962674 50683904 11410 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12374 11410 603 41 0 12333 0
vsize: 49496
[startup+790.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11711 0 0 0 78976 34 0 0 25 0 1 0 478962674 51077120 11507 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12470 11507 603 41 0 12429 0
vsize: 49880
[startup+800.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11821 0 0 0 79976 34 0 0 25 0 1 0 478962674 51474432 11617 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12567 11617 603 41 0 12526 0
vsize: 50268
[startup+810.016 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11897 0 0 0 80976 34 0 0 25 0 1 0 478962674 51863552 11693 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12662 11693 603 41 0 12621 0
vsize: 50648
[startup+820.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 11988 0 0 0 81976 35 0 0 25 0 1 0 478962674 52260864 11784 4294967295 134512640 134672761 3221224640 3221223808 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12759 11784 603 41 0 12718 0
vsize: 51036
[startup+830.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12073 0 0 0 82976 35 0 0 25 0 1 0 478962674 52523008 11869 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12823 11869 603 41 0 12782 0
vsize: 51292
[startup+840.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12162 0 0 0 83976 35 0 0 25 0 1 0 478962674 52912128 11958 4294967295 134512640 134672761 3221224640 3221223824 134558761 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12918 11958 603 41 0 12877 0
vsize: 51672
[startup+850.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12247 0 0 0 84976 35 0 0 25 0 1 0 478962674 53297152 12043 4294967295 134512640 134672761 3221224640 3221223824 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13012 12043 603 41 0 12971 0
vsize: 52048
[startup+860.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12340 0 0 0 85976 35 0 0 25 0 1 0 478962674 53608448 12136 4294967295 134512640 134672761 3221224640 3221223744 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13088 12136 603 41 0 13047 0
vsize: 52352
[startup+870.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12459 0 0 0 86976 36 0 0 25 0 1 0 478962674 54132736 12255 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13216 12255 603 41 0 13175 0
vsize: 52864
[startup+880.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12536 0 0 0 87976 36 0 0 25 0 1 0 478962674 54394880 12332 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13280 12332 603 41 0 13239 0
vsize: 53120
[startup+890.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12610 0 0 0 88976 36 0 0 25 0 1 0 478962674 54792192 12406 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13377 12406 603 41 0 13336 0
vsize: 53508
[startup+900.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12709 0 0 0 89976 37 0 0 25 0 1 0 478962674 55189504 12505 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13474 12505 603 41 0 13433 0
vsize: 53896
[startup+910.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12796 0 0 0 90976 37 0 0 25 0 1 0 478962674 55443456 12592 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13536 12592 603 41 0 13495 0
vsize: 54144
[startup+920.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12868 0 0 0 91976 37 0 0 25 0 1 0 478962674 55840768 12664 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13633 12664 603 41 0 13592 0
vsize: 54532
[startup+930.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 12934 0 0 0 92976 37 0 0 25 0 1 0 478962674 56102912 12730 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13697 12730 603 41 0 13656 0
vsize: 54788
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28567
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13020 0 0 0 93976 37 0 0 25 0 1 0 478962674 56455168 12816 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13783 12816 603 41 0 13742 0
vsize: 55132
[startup+950.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13131 0 0 0 94975 38 0 0 25 0 1 0 478962674 56852480 12927 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13880 12927 603 41 0 13839 0
vsize: 55520
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13245 0 0 0 95975 38 0 0 25 0 1 0 478962674 57384960 13041 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14010 13041 603 41 0 13969 0
vsize: 56040
[startup+970.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13358 0 0 0 96974 39 0 0 25 0 1 0 478962674 57782272 13154 4294967295 134512640 134672761 3221224640 3221223744 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14107 13154 603 41 0 14066 0
vsize: 56428
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13462 0 0 0 97974 39 0 0 25 0 1 0 478962674 58175488 13258 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14203 13258 603 41 0 14162 0
vsize: 56812
[startup+990.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13552 0 0 0 98974 39 0 0 25 0 1 0 478962674 58564608 13348 4294967295 134512640 134672761 3221224640 3221223824 134558846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14298 13348 603 41 0 14257 0
vsize: 57192
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13647 0 0 0 99974 40 0 0 25 0 1 0 478962674 58949632 13443 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14392 13443 603 41 0 14351 0
vsize: 57568
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13739 0 0 0 100974 40 0 0 25 0 1 0 478962674 59342848 13535 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14488 13535 603 41 0 14447 0
vsize: 57952
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13837 0 0 0 101973 41 0 0 25 0 1 0 478962674 59736064 13633 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14584 13633 603 41 0 14543 0
vsize: 58336
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 13939 0 0 0 102973 41 0 0 25 0 1 0 478962674 60129280 13735 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14680 13735 603 41 0 14639 0
vsize: 58720
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 103973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 104973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 105973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223824 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 106973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 107973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 108973 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 109974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 110974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 111974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223776 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 112974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 113974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223744 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 114974 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 115975 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 116975 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 117975 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 118975 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 28569
Raw data (stat): 28512 (minisat+) R 28511 26298 26297 0 -1 0 14029 0 0 0 119975 42 0 0 25 0 1 0 478962674 60522496 13825 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14776 13825 603 41 0 14735 0
vsize: 59104
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 28569
Raw data (stat): 28512 (minisat+) Z 28511 26298 26297 0 -1 12 14032 0 0 0 119976 44 0 0 25 0 1 0 478962674 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.05
CPU time (s): 1200.21
CPU user time (s): 1199.76
CPU system time (s): 0.448931
CPU usage (%): 100.014
Max. virtual memory (Kb): 59104
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####