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 5894

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        878104 kB
Buffers:         37508 kB
Cached:          97676 kB
SwapCached:          0 kB
Active:          73468 kB
Inactive:        66420 kB
HighTotal:      131008 kB
HighFree:        27636 kB
LowTotal:       903652 kB
LowFree:        850468 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11084 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 02:33:08 (client local time) WITH STATUS 10 IN 1209.96 SECONDS
stats: 4304 7 1209.96 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.98 0.95 0.91 2/54 32498
Raw data (stat): 32498 (runsolver) R 32497 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 409113422 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 4329 0 0 0 989 10 0 0 25 0 1 0 409113422 19595264 4152 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4784 4152 603 41 0 4743 0
vsize: 19136
[startup+20.0014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 4563 0 0 0 1987 11 0 0 25 0 1 0 409113422 20910080 4386 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5105 4386 603 41 0 5064 0
vsize: 20420
[startup+30.0017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 4745 0 0 0 2986 12 0 0 25 0 1 0 409113422 21561344 4568 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5264 4568 603 41 0 5223 0
vsize: 21056
[startup+40.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5003 0 0 0 3985 14 0 0 25 0 1 0 409113422 22700032 4826 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5542 4826 603 41 0 5501 0
vsize: 22168
[startup+50.0032 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5205 0 0 0 4983 15 0 0 25 0 1 0 409113422 23502848 5028 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5738 5028 603 41 0 5697 0
vsize: 22952
[startup+60.004 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5370 0 0 0 5982 16 0 0 25 0 1 0 409113422 24211456 5193 4294967295 134512640 134672761 3221224560 3221223684 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5911 5193 603 41 0 5870 0
vsize: 23644
[startup+70.0043 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5528 0 0 0 6981 17 0 0 25 0 1 0 409113422 24875008 5351 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6073 5351 603 41 0 6032 0
vsize: 24292
[startup+80.0041 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5603 0 0 0 7981 17 0 0 25 0 1 0 409113422 25141248 5426 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6138 5426 603 41 0 6097 0
vsize: 24552
[startup+90.0043 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5720 0 0 0 8980 18 0 0 25 0 1 0 409113422 25673728 5543 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6268 5543 603 41 0 6227 0
vsize: 25072
[startup+100.004 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 5911 0 0 0 9979 19 0 0 25 0 1 0 409113422 26460160 5734 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6460 5734 603 41 0 6419 0
vsize: 25840
[startup+110.005 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6071 0 0 0 10978 20 0 0 25 0 1 0 409113422 27127808 5894 4294967295 134512640 134672761 3221224560 3221223728 134561391 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6623 5894 603 41 0 6582 0
vsize: 26492
[startup+120.006 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6223 0 0 0 11978 20 0 0 25 0 1 0 409113422 27656192 6046 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6752 6046 603 41 0 6711 0
vsize: 27008
[startup+130.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6411 0 0 0 12977 21 0 0 25 0 1 0 409113422 28454912 6234 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6947 6234 603 41 0 6906 0
vsize: 27788
[startup+140.005 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6589 0 0 0 13976 22 0 0 25 0 1 0 409113422 29245440 6412 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7140 6412 603 41 0 7099 0
vsize: 28560
[startup+150.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6779 0 0 0 14975 23 0 0 25 0 1 0 409113422 30044160 6602 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7335 6602 603 41 0 7294 0
vsize: 29340
[startup+160.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 6906 0 0 0 15974 23 0 0 25 0 1 0 409113422 30568448 6729 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7463 6729 603 41 0 7422 0
vsize: 29852
[startup+170.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7071 0 0 0 16974 24 0 0 25 0 1 0 409113422 31236096 6894 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7626 6894 603 41 0 7585 0
vsize: 30504
[startup+180.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7229 0 0 0 17973 24 0 0 25 0 1 0 409113422 31887360 7052 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7785 7052 603 41 0 7744 0
vsize: 31140
[startup+190.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7409 0 0 0 18972 25 0 0 25 0 1 0 409113422 32677888 7232 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7978 7232 603 41 0 7937 0
vsize: 31912
[startup+200.006 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7598 0 0 0 19971 26 0 0 25 0 1 0 409113422 33333248 7421 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8138 7421 603 41 0 8097 0
vsize: 32552
[startup+210.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7746 0 0 0 20970 27 0 0 25 0 1 0 409113422 34000896 7569 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8301 7569 603 41 0 8260 0
vsize: 33204
[startup+220.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 7893 0 0 0 21969 28 0 0 25 0 1 0 409113422 34533376 7716 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8431 7716 603 41 0 8390 0
vsize: 33724
[startup+230.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8045 0 0 0 22969 29 0 0 25 0 1 0 409113422 35192832 7868 4294967295 134512640 134672761 3221224560 3221223664 134559922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8592 7868 603 41 0 8551 0
vsize: 34368
[startup+240.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8196 0 0 0 23968 29 0 0 25 0 1 0 409113422 35856384 8019 4294967295 134512640 134672761 3221224560 3221223664 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8754 8019 603 41 0 8713 0
vsize: 35016
[startup+250.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8361 0 0 0 24967 30 0 0 25 0 1 0 409113422 36524032 8184 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8917 8184 603 41 0 8876 0
vsize: 35668
[startup+260.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8531 0 0 0 25966 31 0 0 25 0 1 0 409113422 37187584 8354 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9079 8354 603 41 0 9038 0
vsize: 36316
[startup+270.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8684 0 0 0 26965 32 0 0 25 0 1 0 409113422 37855232 8507 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9242 8507 603 41 0 9201 0
vsize: 36968
[startup+280.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8824 0 0 0 27964 33 0 0 25 0 1 0 409113422 38371328 8647 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9368 8647 603 41 0 9327 0
vsize: 37472
[startup+290.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 8982 0 0 0 28962 34 0 0 25 0 1 0 409113422 39030784 8805 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9529 8805 603 41 0 9488 0
vsize: 38116
[startup+300.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 29961 35 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+310.01 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 30961 35 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+320.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 31961 36 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223760 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+330.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 32960 36 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+340.011 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 33960 37 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+350.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 34959 37 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+360.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 35959 37 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+370.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 36958 38 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+380.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 37958 38 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+390.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 38958 38 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223696 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+400.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 39957 39 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+410.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 40957 39 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+420.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 41957 39 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+430.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 42956 40 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+440.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 43956 40 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+450.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 44956 40 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+460.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 45955 41 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+470.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9024 0 0 0 46955 41 0 0 25 0 1 0 409113422 39165952 8847 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8847 603 41 0 9521 0
vsize: 38248
[startup+480.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 47955 41 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223696 134560557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+490.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 48955 41 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+500.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 49954 41 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+510.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 50954 42 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+520.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 51954 42 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+530.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9025 0 0 0 52953 43 0 0 25 0 1 0 409113422 39165952 8848 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9562 8848 603 41 0 9521 0
vsize: 38248
[startup+540.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9067 0 0 0 53952 43 0 0 25 0 1 0 409113422 39424000 8890 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9625 8890 603 41 0 9584 0
vsize: 38500
[startup+550.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9170 0 0 0 54952 43 0 0 25 0 1 0 409113422 39825408 8993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9723 8993 603 41 0 9682 0
vsize: 38892
[startup+560.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9269 0 0 0 55951 44 0 0 25 0 1 0 409113422 40218624 9092 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9819 9092 603 41 0 9778 0
vsize: 39276
[startup+570.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9359 0 0 0 56951 44 0 0 25 0 1 0 409113422 40615936 9182 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9916 9182 603 41 0 9875 0
vsize: 39664
[startup+580.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9464 0 0 0 57950 45 0 0 25 0 1 0 409113422 41005056 9287 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10011 9287 603 41 0 9970 0
vsize: 40044
[startup+590.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9556 0 0 0 58950 45 0 0 25 0 1 0 409113422 41406464 9379 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10109 9379 603 41 0 10068 0
vsize: 40436
[startup+600.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9640 0 0 0 59950 45 0 0 25 0 1 0 409113422 41672704 9463 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10174 9463 603 41 0 10133 0
vsize: 40696
[startup+610.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9724 0 0 0 60948 46 0 0 25 0 1 0 409113422 42078208 9547 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10273 9547 603 41 0 10232 0
vsize: 41092
[startup+620.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9834 0 0 0 61948 47 0 0 25 0 1 0 409113422 42737664 9657 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10434 9657 603 41 0 10393 0
vsize: 41736
[startup+630.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 9934 0 0 0 62947 48 0 0 25 0 1 0 409113422 43126784 9757 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10529 9757 603 41 0 10488 0
vsize: 42116
[startup+640.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10040 0 0 0 63946 48 0 0 25 0 1 0 409113422 43651072 9863 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10657 9863 603 41 0 10616 0
vsize: 42628
[startup+650.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10122 0 0 0 64946 49 0 0 25 0 1 0 409113422 43917312 9945 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10722 9945 603 41 0 10681 0
vsize: 42888
[startup+660.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10211 0 0 0 65945 49 0 0 25 0 1 0 409113422 44355584 10034 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10829 10034 603 41 0 10788 0
vsize: 43316
[startup+670.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10334 0 0 0 66944 50 0 0 25 0 1 0 409113422 44879872 10157 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 10157 603 41 0 10916 0
vsize: 43828
[startup+680.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10443 0 0 0 67943 51 0 0 25 0 1 0 409113422 45301760 10266 4294967295 134512640 134672761 3221224560 3221223696 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11060 10266 603 41 0 11019 0
vsize: 44240
[startup+690.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10549 0 0 0 68943 52 0 0 25 0 1 0 409113422 45686784 10372 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11154 10372 603 41 0 11113 0
vsize: 44616
[startup+700.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10658 0 0 0 69942 52 0 0 25 0 1 0 409113422 46211072 10481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11282 10481 603 41 0 11241 0
vsize: 45128
[startup+710.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10765 0 0 0 70942 52 0 0 25 0 1 0 409113422 46600192 10588 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11377 10588 603 41 0 11336 0
vsize: 45508
[startup+720.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10869 0 0 0 71942 53 0 0 25 0 1 0 409113422 47005696 10692 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11476 10692 603 41 0 11435 0
vsize: 45904
[startup+730.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 10953 0 0 0 72941 53 0 0 25 0 1 0 409113422 47394816 10776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11571 10776 603 41 0 11530 0
vsize: 46284
[startup+740.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11036 0 0 0 73940 54 0 0 25 0 1 0 409113422 47652864 10859 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11634 10859 603 41 0 11593 0
vsize: 46536
[startup+750.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11154 0 0 0 74940 54 0 0 25 0 1 0 409113422 48185344 10977 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11764 10977 603 41 0 11723 0
vsize: 47056
[startup+760.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11256 0 0 0 75939 55 0 0 25 0 1 0 409113422 48582656 11079 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11079 603 41 0 11820 0
vsize: 47444
[startup+770.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11350 0 0 0 76939 55 0 0 25 0 1 0 409113422 48971776 11173 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11956 11173 603 41 0 11915 0
vsize: 47824
[startup+780.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11447 0 0 0 77938 56 0 0 25 0 1 0 409113422 49369088 11270 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12053 11270 603 41 0 12012 0
vsize: 48212
[startup+790.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11548 0 0 0 78937 57 0 0 25 0 1 0 409113422 49758208 11371 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12148 11371 603 41 0 12107 0
vsize: 48592
[startup+800.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11642 0 0 0 79936 58 0 0 25 0 1 0 409113422 50155520 11465 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12245 11465 603 41 0 12204 0
vsize: 48980
[startup+810.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11749 0 0 0 80936 58 0 0 25 0 1 0 409113422 50548736 11572 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12341 11572 603 41 0 12300 0
vsize: 49364
[startup+820.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11826 0 0 0 81935 59 0 0 25 0 1 0 409113422 50937856 11649 4294967295 134512640 134672761 3221224560 3221223704 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12436 11649 603 41 0 12395 0
vsize: 49744
[startup+830.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11917 0 0 0 82935 59 0 0 25 0 1 0 409113422 51339264 11740 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12534 11740 603 41 0 12493 0
vsize: 50136
[startup+840.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 11998 0 0 0 83934 60 0 0 25 0 1 0 409113422 51597312 11821 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12597 11821 603 41 0 12556 0
vsize: 50388
[startup+850.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12091 0 0 0 84934 60 0 0 25 0 1 0 409113422 51994624 11914 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12694 11914 603 41 0 12653 0
vsize: 50776
[startup+860.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12170 0 0 0 85933 61 0 0 25 0 1 0 409113422 52252672 11993 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12757 11993 603 41 0 12716 0
vsize: 51028
[startup+870.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12263 0 0 0 86933 61 0 0 25 0 1 0 409113422 52662272 12086 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12857 12086 603 41 0 12816 0
vsize: 51428
[startup+880.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12386 0 0 0 87932 62 0 0 25 0 1 0 409113422 53194752 12209 4294967295 134512640 134672761 3221224560 3221223728 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12987 12209 603 41 0 12946 0
vsize: 51948
[startup+890.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12458 0 0 0 88931 62 0 0 25 0 1 0 409113422 53456896 12281 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13051 12281 603 41 0 13010 0
vsize: 52204
[startup+900.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12530 0 0 0 89931 63 0 0 25 0 1 0 409113422 53841920 12353 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13145 12353 603 41 0 13104 0
vsize: 52580
[startup+910.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12630 0 0 0 90930 63 0 0 25 0 1 0 409113422 54235136 12453 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13241 12453 603 41 0 13200 0
vsize: 52964
[startup+920.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12717 0 0 0 91930 63 0 0 25 0 1 0 409113422 54493184 12540 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13304 12540 603 41 0 13263 0
vsize: 53216
[startup+930.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12787 0 0 0 92930 64 0 0 25 0 1 0 409113422 54755328 12610 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13368 12610 603 41 0 13327 0
vsize: 53472
[startup+940.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12853 0 0 0 93929 64 0 0 25 0 1 0 409113422 55021568 12676 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13433 12676 603 41 0 13392 0
vsize: 53732
[startup+950.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 12937 0 0 0 94929 64 0 0 25 0 1 0 409113422 55500800 12760 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13550 12760 603 41 0 13509 0
vsize: 54200
[startup+960.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13048 0 0 0 95928 65 0 0 25 0 1 0 409113422 55898112 12871 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13647 12871 603 41 0 13606 0
vsize: 54588
[startup+970.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13162 0 0 0 96928 66 0 0 25 0 1 0 409113422 56295424 12985 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13744 12985 603 41 0 13703 0
vsize: 54976
[startup+980.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13276 0 0 0 97927 66 0 0 25 0 1 0 409113422 56823808 13099 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13873 13099 603 41 0 13832 0
vsize: 55492
[startup+990.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13377 0 0 0 98927 66 0 0 25 0 1 0 409113422 57225216 13200 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13971 13200 603 41 0 13930 0
vsize: 55884
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13467 0 0 0 99926 67 0 0 25 0 1 0 409113422 57614336 13290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14066 13290 603 41 0 14025 0
vsize: 56264
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13562 0 0 0 100925 68 0 0 25 0 1 0 409113422 58011648 13385 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14163 13385 603 41 0 14122 0
vsize: 56652
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13649 0 0 0 101925 68 0 0 25 0 1 0 409113422 58269696 13472 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14226 13472 603 41 0 14185 0
vsize: 56904
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13749 0 0 0 102924 69 0 0 25 0 1 0 409113422 58798080 13572 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14355 13572 603 41 0 14314 0
vsize: 57420
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13844 0 0 0 103924 69 0 0 25 0 1 0 409113422 59060224 13667 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14419 13667 603 41 0 14378 0
vsize: 57676
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 104924 69 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 105923 69 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 106923 70 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 107922 70 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 108922 71 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 109921 71 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 110921 71 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 111921 72 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13951 0 0 0 112920 72 0 0 25 0 1 0 409113422 59588608 13774 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13774 603 41 0 14507 0
vsize: 58192
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 113920 73 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223736 134559668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 114919 73 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 115919 73 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 116919 73 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 117918 74 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 118918 74 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 119918 74 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
[startup+1210.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 32498
Raw data (stat): 32498 (minisat+) R 32497 26667 26666 0 -1 0 13957 0 0 0 120918 74 0 0 25 0 1 0 409113422 59588608 13780 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13780 603 41 0 14507 0
vsize: 58192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 32498
Raw data (stat): 32498 (minisat+) Z 32497 26667 26666 0 -1 12 13960 0 0 0 120918 77 0 0 25 0 1 0 409113422 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): 1210.08
CPU time (s): 1209.96
CPU user time (s): 1209.18
CPU system time (s): 0.775882
CPU usage (%): 99.99
Max. virtual memory (Kb): 58192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####