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-ii8d1.opb
MD5SUM	f5ae067eec5cb4736f6ec50c87e4a015
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	343
Optimality of the best value was proved	NO
Number of terms in the objective function	1060
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	1060
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	1060
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.05184
Number of variables	1060
Total number of constraints	3737
Number of constraints which are clauses	3737
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	10
Trace number 6269

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 04:03:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4685 boxname=wulflinc15 idbench=173 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f5ae067eec5cb4736f6ec50c87e4a015  /oldhome/oroussel/tmp/wulflinc15/normalized-ii8d1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-ii8d1.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ii8d1.opb
IDLAUNCH: 4685
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        892900 kB
Buffers:         36720 kB
Cached:          83332 kB
SwapCached:       2144 kB
Active:          64724 kB
Inactive:        60336 kB
HighTotal:      131008 kB
HighFree:        43792 kB
LowTotal:       903652 kB
LowFree:        849108 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 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 04:23:50 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 4685 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3737 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 |    3737     8550 |    1245       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 394[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:57992     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         5 |  140267   327780 |   46755       5       53    10.6 |  0.000 % |
c |       105 |  140267   327780 |   51430     105      992     9.4 |  0.024 % |
c |       255 |  134666   314817 |   56573     147     2361    16.1 |  3.666 % |
c |       480 |  132534   309921 |   62230     334     5317    15.9 |  5.069 % |
c |       817 |  130922   306250 |   68453     560    13156    23.5 |  6.078 % |
c |      1324 |  120339   281904 |   75299     925    21654    23.4 | 13.131 % |
c |      2084 |  108036   253515 |   82829    1365    27710    20.3 | 21.526 % |
c |      3223 |  107415   252090 |   91112    2496    57283    22.9 | 21.932 % |
c |      4935 |   95425   224443 |  100223    4048   128483    31.7 | 29.975 % |
c |      7498 |   77729   183506 |  110245    6277   190295    30.3 | 42.048 % |
c |     11342 |   64225   152171 |  121270    9887   384384    38.9 | 51.517 % |
c |     17108 |   62613   148418 |  133397   15591   668172    42.9 | 52.669 % |
c |     25757 |   60248   142924 |  146737   24130  1236324    51.2 | 54.323 % |
c |     38731 |   60248   142924 |  161410   37104  1986958    53.6 | 54.323 % |
c ==============================================================================
c [1mFound solution: 393[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 |     44868 |   60178   142790 |   20059   43216  2363826    54.7 | 54.323 % |
c |     44968 |   60178   142790 |   22064   43316  2367484    54.7 | 54.433 % |
c |     45118 |   60090   142586 |   24271   43462  2369108    54.5 | 54.496 % |
c |     45344 |   60090   142586 |   26698   43688  2376006    54.4 | 54.496 % |
c |     45684 |   60090   142586 |   29368   44028  2381056    54.1 | 54.496 % |
c |     46191 |   59981   142336 |   32305   44531  2391298    53.7 | 54.567 % |
c |     46952 |   59799   141918 |   35535   45280  2446423    54.0 | 54.686 % |
c |     48092 |   59551   141343 |   39089   46406  2466587    53.2 | 54.852 % |
c |     49802 |   59458   141125 |   42998   48097  2573502    53.5 | 54.924 % |
c |     52365 |   59365   140911 |   47298   50658  2655170    52.4 | 54.986 % |
c |     56209 |   59365   140911 |   52027   54502  2817259    51.7 | 54.986 % |
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 |     59005 |   59578   141447 |   19859   57298  3034022    53.0 | 54.986 % |
c |     59105 |   59511   141293 |   21844   17257   615150    35.6 | 54.970 % |
c |     59255 |   59511   141293 |   24029   17407   616135    35.4 | 54.970 % |
c |     59480 |   59422   141086 |   26432   17627   622676    35.3 | 55.031 % |
c |     59818 |   59359   140940 |   29075   17964   626377    34.9 | 55.076 % |
c |     60324 |   59349   140917 |   31983   18466   633263    34.3 | 55.082 % |
c |     61083 |   59349   140917 |   35181   19225   647375    33.7 | 55.082 % |
c |     62222 |   59276   140749 |   38699   20360   676412    33.2 | 55.132 % |
c |     63932 |   59276   140749 |   42569   22070   734070    33.3 | 55.132 % |
c ==============================================================================
c [1mFound solution: 386[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 |     64558 |   59226   140620 |   19742   22614   746773    33.0 | 55.132 % |
c |     64658 |   59226   140620 |   21716   22714   749605    33.0 | 55.156 % |
c |     64808 |   59226   140620 |   23887   22864   764721    33.4 | 55.156 % |
c |     65033 |   59226   140620 |   26276   23089   769364    33.3 | 55.156 % |
c |     65371 |   59226   140620 |   28904   23427   779591    33.3 | 55.156 % |
c |     65878 |   59226   140620 |   31794   23934   800960    33.5 | 55.156 % |
c |     66638 |   59226   140620 |   34974   24694   931173    37.7 | 55.156 % |
c |     67777 |   59226   140620 |   38471   25833   969353    37.5 | 55.156 % |
c |     69485 |   59226   140620 |   42318   27541  1121065    40.7 | 55.156 % |
c |     72047 |   59226   140620 |   46550   30103  1235182    41.0 | 55.156 % |
c |     75892 |   59226   140620 |   51205   33948  1344043    39.6 | 55.156 % |
c |     81659 |   59226   140620 |   56326   39715  2591954    65.3 | 55.156 % |
c |     90309 |   59047   140208 |   61958   48217  3285228    68.1 | 55.272 % |
c |    103283 |   58569   139088 |   68154   61138  4378855    71.6 | 55.624 % |
c |    122744 |   58569   139088 |   74970   80599  8386096   104.0 | 55.624 % |
c |    151939 |   58350   138578 |   82467   26513  3532839   133.2 | 55.785 % |
c |    195728 |   58256   138359 |   90713   70237 11924539   169.8 | 55.854 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1 -x2 -x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 -x23 x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 -x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 x43 -x44 -x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 -x55 x56 x57 -x58 -x59 -x60 -x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 -x79 x80 x81 -x82 -x83 x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 -x95 x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 -x107 x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 -x123 x124 x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 -x151 x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 -x167 x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 -x199 x200 x201 -x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 x219 -x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 -x247 x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 -x263 x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 x279 -x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 -x295 x296 x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 x307 -x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 x319 -x320 -x321 x322 -x323 x324 -x325 -x326 x327 -x328 -x329 x330 -x331 x332 -x333 x334 -x335 x336 -x337 x338 -x339 x340 -x341 -x342 -x343 -x344 -x345 x346 -x347 x348 x349 -x350 -x351 x352 -x353 x354 -x355 -x356 -x357 x358 -x359 x360 -x361 -x362 -x363 -x364 -x365 x366 -x367 x368 -x369 -x370 -x371 x372 -x373 x374 x375 -x376 -x377 x378 -x379 x380 -x381 x382 -x383 x384 -x385 x386 x387 -x388 -x389 x390 -x391 x392 -x393 x394 -x395 x396 -x397 x398 -x399 x400 x401 -x402 -x403 x404 -x405 x406 -x407 x408 -x409 -x410 -x411 x412 -x413 x414 -x415 -x416 -x417 x418 -x419 x420 -x421 x422 -x423 x424 -x425 x426 -x427 x428 -x429 -x430 -x431 x432 -x433 x434 x435 -x436 -x437 x438 -x439 x440 -x441 x442 -x443 x444 -x445 -x446 -x447 x448 -x449 x450 x451 -x452 -x453 -x454 -x455 x456 -x457 -x458 -x459 -x460 -x461 x462 -x463 x464 -x465 x466 -x467 x468 x469 -x470 -x471 -x472 -x473 -x474 -x475 -x476 -x477 -x478 -x479 -x480 -x481 x482 -x483 x484 -x485 x486 -x487 x488 -x489 x490 -x491 -x492 -x493 -x494 -x495 x496 x497 -x498 -x499 -x500 -x501 x502 -x503 x504 x505 -x506 -x507 x508 -x509 x510 -x511 -x512 -x513 -x514 -x515 x516 -x517 -x518 -x519 -x520 -x521 x522 -x523 x524 -x525 x526 -x527 x528 -x529 x530 -x531 -x532 -x533 -x534 -x535 x536 -x537 -x538 x539 -x540 -x541 x542 -x543 x544 -x545 x546 -x547 x548 x549 -x550 -x551 x552 -x553 x554 -x555 -x556 -x557 x558 -x559 x560 -x561 x562 -x563 x564 x565 -x566 -x567 x568 -x569 -x570 -x571 x572 -x573 x574 -x575 -x576 -x577 x578 -x579 x580 x581 -x582 -x583 x584 -x585 x586 -x587 x588 -x589 -x590 -x591 x592 -x593 x594 -x595 -x596 -x597 x598 -x599 x600 -x601 x602 -x603 x604 -x605 x606 -x607 x608 -x609 -x610 -x611 -x612 x613 -x614 -x615 -x616 -x617 -x618 -x619 -x620 -x621 -x622 -x623 x624 -x625 -x626 x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 -x637 -x638 -x639 -x640 -x641 -x642 -x643 x644 -x645 x646 -x647 -x648 x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 -x657 -x658 -x659 -x660 -x661 x662 -x663 x664 -x665 x666 x667 -x668 -x669 x670 -x671 -x672 -x673 -x674 -x675 x676 -x677 -x678 -x679 -x680 -x681 x682 -x683 x684 -x685 x686 x687 -x688 -x689 x690 -x691 x692 -x693 x694 -x695 x696 -x697 x698 -x699 x700 -x701 x702 -x703 x704 -x705 -x706 -x707 x708 -x709 x710 -x711 -x712 x713 -x714 -x715 x716 -x717 -x718 -x719 -x720 -x721 x722 -x723 x724 -x725 x726 -x727 x728 -x729 x730 -x731 -x732 -x733 -x734 -x735 x736 -x737 -x738 x739 -x740 x741 -x742 -x743 x744 #### 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.92 0.95 0.90 2/54 4863
Raw data (stat): 4863 (runsolver) R 4862 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423340229 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.0012 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4357 0 0 0 986 12 0 0 25 0 1 0 423340229 20365312 4181 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4972 4181 603 41 0 4931 0
vsize: 19888
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4376 0 0 0 1986 12 0 0 25 0 1 0 423340229 20365312 4200 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4972 4200 603 41 0 4931 0
vsize: 19888
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4462 0 0 0 2986 12 0 0 25 0 1 0 423340229 20762624 4286 4294967295 134512640 134672761 3221224576 3221223756 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5069 4286 603 41 0 5028 0
vsize: 20276
[startup+40.0026 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4499 0 0 0 3986 12 0 0 25 0 1 0 423340229 20893696 4323 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5101 4323 603 41 0 5060 0
vsize: 20404
[startup+50.003 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4607 0 0 0 4985 13 0 0 25 0 1 0 423340229 21311488 4431 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5203 4431 603 41 0 5162 0
vsize: 20812
[startup+60.0028 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4724 0 0 0 5985 13 0 0 25 0 1 0 423340229 21889024 4548 4294967295 134512640 134672761 3221224576 3221223760 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5344 4548 603 41 0 5303 0
vsize: 21376
[startup+70.003 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 4900 0 0 0 6985 14 0 0 25 0 1 0 423340229 22564864 4724 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5509 4724 603 41 0 5468 0
vsize: 22036
[startup+80.0035 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 5162 0 0 0 7984 14 0 0 25 0 1 0 423340229 23625728 4986 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5768 4986 603 41 0 5727 0
vsize: 23072
[startup+90.0033 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 5338 0 0 0 8984 15 0 0 25 0 1 0 423340229 24424448 5162 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5963 5162 603 41 0 5922 0
vsize: 23852
[startup+100.004 s]
Raw data (loadavg): 1.34 1.06 0.94 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 5525 0 0 0 9983 16 0 0 25 0 1 0 423340229 25096192 5349 4294967295 134512640 134672761 3221224576 3221223680 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6127 5349 603 41 0 6086 0
vsize: 24508
[startup+110.004 s]
Raw data (loadavg): 1.29 1.05 0.94 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 5820 0 0 0 10982 17 0 0 25 0 1 0 423340229 26304512 5644 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6422 5644 603 41 0 6381 0
vsize: 25688
[startup+120.004 s]
Raw data (loadavg): 1.24 1.05 0.94 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 6081 0 0 0 11981 18 0 0 25 0 1 0 423340229 27365376 5905 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6681 5905 603 41 0 6640 0
vsize: 26724
[startup+130.005 s]
Raw data (loadavg): 1.20 1.05 0.94 2/54 4863
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 6325 0 0 0 12980 19 0 0 25 0 1 0 423340229 28430336 6149 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6941 6149 603 41 0 6900 0
vsize: 27764
[startup+140.005 s]
Raw data (loadavg): 1.17 1.05 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 6606 0 0 0 13979 21 0 0 25 0 1 0 423340229 29638656 6430 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7236 6430 603 41 0 7195 0
vsize: 28944
[startup+150.005 s]
Raw data (loadavg): 1.15 1.05 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 6794 0 0 0 14979 21 0 0 25 0 1 0 423340229 30445568 6618 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7433 6618 603 41 0 7392 0
vsize: 29732
[startup+160.005 s]
Raw data (loadavg): 1.12 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7109 0 0 0 15978 22 0 0 25 0 1 0 423340229 31916032 6933 4294967295 134512640 134672761 3221224576 3221223680 134560364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7792 6933 603 41 0 7751 0
vsize: 31168
[startup+170.006 s]
Raw data (loadavg): 1.10 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7248 0 0 0 16978 22 0 0 25 0 1 0 423340229 32456704 7072 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7924 7072 603 41 0 7883 0
vsize: 31696
[startup+180.007 s]
Raw data (loadavg): 1.09 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7415 0 0 0 17977 23 0 0 25 0 1 0 423340229 33124352 7239 4294967295 134512640 134672761 3221224576 3221223744 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8087 7239 603 41 0 8046 0
vsize: 32348
[startup+190.007 s]
Raw data (loadavg): 1.07 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7588 0 0 0 18976 24 0 0 25 0 1 0 423340229 33935360 7412 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8285 7412 603 41 0 8244 0
vsize: 33140
[startup+200.007 s]
Raw data (loadavg): 1.06 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 19975 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+210.007 s]
Raw data (loadavg): 1.05 1.04 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 20976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223700 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+220.007 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 21976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+230.008 s]
Raw data (loadavg): 1.04 1.03 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 22976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+240.008 s]
Raw data (loadavg): 1.03 1.03 0.94 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 23976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+250.008 s]
Raw data (loadavg): 1.10 1.04 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 24976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+260.008 s]
Raw data (loadavg): 1.08 1.04 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 25976 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+270.008 s]
Raw data (loadavg): 1.07 1.04 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 26977 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223712 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+280.01 s]
Raw data (loadavg): 1.06 1.04 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 27977 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223680 134559808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+290.01 s]
Raw data (loadavg): 1.05 1.04 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 7850 0 0 0 28977 25 0 0 25 0 1 0 423340229 34877440 7674 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8515 7674 603 41 0 8474 0
vsize: 34060
[startup+300.01 s]
Raw data (loadavg): 1.04 1.03 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8103 0 0 0 29976 25 0 0 25 0 1 0 423340229 35938304 7927 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8774 7927 603 41 0 8733 0
vsize: 35096
[startup+310.01 s]
Raw data (loadavg): 1.11 1.05 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8331 0 0 0 30976 26 0 0 25 0 1 0 423340229 36847616 8155 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8996 8155 603 41 0 8955 0
vsize: 35984
[startup+320.01 s]
Raw data (loadavg): 1.09 1.05 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8383 0 0 0 31976 26 0 0 25 0 1 0 423340229 37113856 8207 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9061 8207 603 41 0 9020 0
vsize: 36244
[startup+330.011 s]
Raw data (loadavg): 1.08 1.05 0.95 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8567 0 0 0 32976 27 0 0 25 0 1 0 423340229 37916672 8391 4294967295 134512640 134672761 3221224576 3221223744 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9257 8391 603 41 0 9216 0
vsize: 37028
[startup+340.011 s]
Raw data (loadavg): 1.14 1.06 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8756 0 0 0 33976 27 0 0 25 0 1 0 423340229 38580224 8580 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9419 8580 603 41 0 9378 0
vsize: 37676
[startup+350.011 s]
Raw data (loadavg): 1.12 1.06 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 8955 0 0 0 34975 28 0 0 25 0 1 0 423340229 39514112 8779 4294967295 134512640 134672761 3221224576 3221223736 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9647 8779 603 41 0 9606 0
vsize: 38588
[startup+360.012 s]
Raw data (loadavg): 1.10 1.06 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 9258 0 0 0 35975 28 0 0 25 0 1 0 423340229 40701952 9082 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9937 9082 603 41 0 9896 0
vsize: 39748
[startup+370.012 s]
Raw data (loadavg): 1.08 1.05 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 9459 0 0 0 36974 29 0 0 25 0 1 0 423340229 41504768 9283 4294967295 134512640 134672761 3221224576 3221223776 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10133 9283 603 41 0 10092 0
vsize: 40532
[startup+380.012 s]
Raw data (loadavg): 1.07 1.05 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 9710 0 0 0 37974 30 0 0 25 0 1 0 423340229 42582016 9534 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10396 9534 603 41 0 10355 0
vsize: 41584
[startup+390.013 s]
Raw data (loadavg): 1.06 1.05 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 10061 0 0 0 38972 31 0 0 25 0 1 0 423340229 44171264 9885 4294967295 134512640 134672761 3221224576 3221223744 134560849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10784 9885 603 41 0 10743 0
vsize: 43136
[startup+400.013 s]
Raw data (loadavg): 1.05 1.05 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 10427 0 0 0 39971 33 0 0 25 0 1 0 423340229 45768704 10251 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11174 10251 603 41 0 11133 0
vsize: 44696
[startup+410.014 s]
Raw data (loadavg): 1.04 1.05 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 10749 0 0 0 40970 34 0 0 25 0 1 0 423340229 46972928 10573 4294967295 134512640 134672761 3221224576 3221223744 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11468 10573 603 41 0 11427 0
vsize: 45872
[startup+420.013 s]
Raw data (loadavg): 1.03 1.04 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 11119 0 0 0 41969 35 0 0 25 0 1 0 423340229 48582656 10943 4294967295 134512640 134672761 3221224576 3221223680 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11861 10943 603 41 0 11820 0
vsize: 47444
[startup+430.015 s]
Raw data (loadavg): 1.03 1.04 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 11480 0 0 0 42968 36 0 0 25 0 1 0 423340229 50049024 11304 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12219 11304 603 41 0 12178 0
vsize: 48876
[startup+440.015 s]
Raw data (loadavg): 1.02 1.04 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 11757 0 0 0 43967 37 0 0 25 0 1 0 423340229 51122176 11581 4294967295 134512640 134672761 3221224576 3221223680 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12481 11581 603 41 0 12440 0
vsize: 49924
[startup+450.015 s]
Raw data (loadavg): 1.02 1.04 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 12031 0 0 0 44967 38 0 0 25 0 1 0 423340229 52322304 11855 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 11855 603 41 0 12733 0
vsize: 51096
[startup+460.016 s]
Raw data (loadavg): 1.02 1.04 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 12272 0 0 0 45966 39 0 0 25 0 1 0 423340229 53243904 12096 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12999 12096 603 41 0 12958 0
vsize: 51996
[startup+470.016 s]
Raw data (loadavg): 1.01 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 12541 0 0 0 46966 39 0 0 25 0 1 0 423340229 54308864 12365 4294967295 134512640 134672761 3221224576 3221223744 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13259 12365 603 41 0 13218 0
vsize: 53036
[startup+480.017 s]
Raw data (loadavg): 1.01 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 12802 0 0 0 47965 40 0 0 25 0 1 0 423340229 55369728 12626 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13518 12626 603 41 0 13477 0
vsize: 54072
[startup+490.018 s]
Raw data (loadavg): 1.01 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 13038 0 0 0 48965 41 0 0 25 0 1 0 423340229 56446976 12862 4294967295 134512640 134672761 3221224576 3221223712 134560654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13781 12862 603 41 0 13740 0
vsize: 55124
[startup+500.018 s]
Raw data (loadavg): 1.01 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 13312 0 0 0 49964 42 0 0 25 0 1 0 423340229 57511936 13136 4294967295 134512640 134672761 3221224576 3221223680 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14041 13136 603 41 0 14000 0
vsize: 56164
[startup+510.019 s]
Raw data (loadavg): 1.00 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 13503 0 0 0 50964 42 0 0 25 0 1 0 423340229 58290176 13327 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14231 13327 603 41 0 14190 0
vsize: 56924
[startup+520.019 s]
Raw data (loadavg): 1.00 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 13647 0 0 0 51963 43 0 0 25 0 1 0 423340229 58826752 13471 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14362 13471 603 41 0 14321 0
vsize: 57448
[startup+530.02 s]
Raw data (loadavg): 1.00 1.03 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 13891 0 0 0 52962 44 0 0 25 0 1 0 423340229 59895808 13715 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14623 13715 603 41 0 14582 0
vsize: 58492
[startup+540.02 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 14195 0 0 0 53961 45 0 0 25 0 1 0 423340229 61100032 14019 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14917 14019 603 41 0 14876 0
vsize: 59668
[startup+550.02 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 14413 0 0 0 54960 46 0 0 25 0 1 0 423340229 62038016 14237 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15146 14237 603 41 0 15105 0
vsize: 60584
[startup+560.02 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 14628 0 0 0 55959 47 0 0 25 0 1 0 423340229 62832640 14452 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15340 14452 603 41 0 15299 0
vsize: 61360
[startup+570.021 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 14852 0 0 0 56958 48 0 0 25 0 1 0 423340229 63746048 14676 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15563 14676 603 41 0 15522 0
vsize: 62252
[startup+580.022 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 15066 0 0 0 57956 49 0 0 25 0 1 0 423340229 64675840 14890 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15790 14890 603 41 0 15749 0
vsize: 63160
[startup+590.022 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 15234 0 0 0 58956 49 0 0 25 0 1 0 423340229 65327104 15058 4294967295 134512640 134672761 3221224576 3221223744 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15949 15058 603 41 0 15908 0
vsize: 63796
[startup+600.022 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 15445 0 0 0 59954 51 0 0 25 0 1 0 423340229 66125824 15269 4294967295 134512640 134672761 3221224576 3221223680 134560408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16144 15269 603 41 0 16103 0
vsize: 64576
[startup+610.023 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 15646 0 0 0 60953 52 0 0 25 0 1 0 423340229 67039232 15470 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16367 15470 603 41 0 16326 0
vsize: 65468
[startup+620.023 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 15836 0 0 0 61952 53 0 0 25 0 1 0 423340229 67833856 15660 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16561 15660 603 41 0 16520 0
vsize: 66244
[startup+630.024 s]
Raw data (loadavg): 1.00 1.02 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 16056 0 0 0 62951 54 0 0 25 0 1 0 423340229 68624384 15880 4294967295 134512640 134672761 3221224576 3221223760 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16754 15880 603 41 0 16713 0
vsize: 67016
[startup+640.025 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 16315 0 0 0 63950 55 0 0 25 0 1 0 423340229 69693440 16139 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17015 16139 603 41 0 16974 0
vsize: 68060
[startup+650.025 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 16535 0 0 0 64949 56 0 0 25 0 1 0 423340229 70623232 16359 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17242 16359 603 41 0 17201 0
vsize: 68968
[startup+660.025 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 16751 0 0 0 65948 57 0 0 25 0 1 0 423340229 71553024 16575 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17469 16575 603 41 0 17428 0
vsize: 69876
[startup+670.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 16982 0 0 0 66947 58 0 0 25 0 1 0 423340229 72486912 16806 4294967295 134512640 134672761 3221224576 3221223680 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17697 16806 603 41 0 17656 0
vsize: 70788
[startup+680.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 17280 0 0 0 67947 58 0 0 25 0 1 0 423340229 73687040 17104 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17990 17104 603 41 0 17949 0
vsize: 71960
[startup+690.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 17560 0 0 0 68946 59 0 0 25 0 1 0 423340229 74752000 17384 4294967295 134512640 134672761 3221224576 3221223760 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18250 17384 603 41 0 18209 0
vsize: 73000
[startup+700.026 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 17765 0 0 0 69945 60 0 0 25 0 1 0 423340229 75665408 17589 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18473 17589 603 41 0 18432 0
vsize: 73892
[startup+710.027 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18005 0 0 0 70944 61 0 0 25 0 1 0 423340229 76591104 17829 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18699 17829 603 41 0 18658 0
vsize: 74796
[startup+720.027 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 71943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223776 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+730.027 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 72943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+740.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 73943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+750.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 74942 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+760.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 75942 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+770.028 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 76942 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223760 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+780.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 77943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+790.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 78943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+800.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 79943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+810.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 80943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+820.029 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 81943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+830.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 82943 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+840.03 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 83944 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+850.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 84944 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+860.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 85944 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134561388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+870.031 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 86944 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+880.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 87944 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+890.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 88945 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+900.032 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 89945 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+910.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 90945 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+920.033 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 91945 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+930.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 92945 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+940.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 93946 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+950.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 94946 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+960.034 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 95946 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+970.046 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 96947 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+980.061 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 97949 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+990.06 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 98949 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 99949 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1010.06 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 100950 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223680 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1020.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 101953 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1030.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 102952 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223744 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1040.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 103952 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1050.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 104952 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1060.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18169 0 0 0 105952 62 0 0 25 0 1 0 423340229 77258752 17993 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18862 17993 603 41 0 18821 0
vsize: 75448
[startup+1070.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18363 0 0 0 106952 63 0 0 25 0 1 0 423340229 78061568 18187 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19058 18187 603 41 0 19017 0
vsize: 76232
[startup+1080.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18676 0 0 0 107951 64 0 0 25 0 1 0 423340229 79372288 18500 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19378 18500 603 41 0 19337 0
vsize: 77512
[startup+1090.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 18997 0 0 0 108951 65 0 0 25 0 1 0 423340229 80699392 18821 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19702 18821 603 41 0 19661 0
vsize: 78808
[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 19312 0 0 0 109950 65 0 0 25 0 1 0 423340229 82030592 19136 4294967295 134512640 134672761 3221224576 3221223680 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20027 19136 603 41 0 19986 0
vsize: 80108
[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 19630 0 0 0 110949 66 0 0 25 0 1 0 423340229 83222528 19454 4294967295 134512640 134672761 3221224576 3221223680 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20318 19454 603 41 0 20277 0
vsize: 81272
[startup+1120.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 19941 0 0 0 111949 67 0 0 25 0 1 0 423340229 84553728 19765 4294967295 134512640 134672761 3221224576 3221223680 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20643 19765 603 41 0 20602 0
vsize: 82572
[startup+1130.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 20244 0 0 0 112949 68 0 0 25 0 1 0 423340229 85749760 20068 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20935 20068 603 41 0 20894 0
vsize: 83740
[startup+1140.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 20516 0 0 0 113948 68 0 0 25 0 1 0 423340229 86958080 20340 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21230 20340 603 41 0 21189 0
vsize: 84920
[startup+1150.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 20781 0 0 0 114948 69 0 0 25 0 1 0 423340229 88031232 20605 4294967295 134512640 134672761 3221224576 3221223680 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21492 20605 603 41 0 21451 0
vsize: 85968
[startup+1160.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 21042 0 0 0 115947 69 0 0 25 0 1 0 423340229 89100288 20866 4294967295 134512640 134672761 3221224576 3221223744 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21753 20866 603 41 0 21712 0
vsize: 87012
[startup+1170.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 21315 0 0 0 116947 70 0 0 25 0 1 0 423340229 90152960 21139 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22010 21139 603 41 0 21969 0
vsize: 88040
[startup+1180.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 21582 0 0 0 117946 71 0 0 25 0 1 0 423340229 91213824 21406 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22269 21406 603 41 0 22228 0
vsize: 89076
[startup+1190.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 21814 0 0 0 118945 72 0 0 25 0 1 0 423340229 92258304 21638 4294967295 134512640 134672761 3221224576 3221223744 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22524 21638 603 41 0 22483 0
vsize: 90096
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 4865
Raw data (stat): 4863 (minisat+) R 4862 29151 29150 0 -1 0 22029 0 0 0 119945 73 0 0 25 0 1 0 423340229 93057024 21853 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22719 21853 603 41 0 22678 0
vsize: 90876
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 1.00 0.96 1/54 4865
Raw data (stat): 4863 (minisat+) Z 4862 29151 29150 0 -1 12 22032 0 0 0 119945 77 0 0 25 0 1 0 423340229 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.16
CPU time (s): 1200.23
CPU user time (s): 1199.46
CPU system time (s): 0.773882
CPU usage (%): 100.006
Max. virtual memory (Kb): 90876
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####