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/logic-synthesis/normalized-max1024.pi.opb
MD5SUM	6604a6c0d979e1f2b09762e6e4f70f84
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	259
Optimality of the best value was proved	NO
Number of terms in the objective function	1278
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	1278
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	1278
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.04584
Number of variables	1278
Total number of constraints	1087
Number of constraints which are clauses	1087
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	1
Maximum length of a constraint	18
Trace number 4822

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-04-13 20:27:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=518 boxname=wulflinc10 idbench=58 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6604a6c0d979e1f2b09762e6e4f70f84  /oldhome/oroussel/tmp/wulflinc10/normalized-max1024.pi.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc10/normalized-max1024.pi.opb
IDLAUNCH: 518
/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:        909792 kB
Buffers:         33876 kB
Cached:          71836 kB
SwapCached:        164 kB
Active:          49276 kB
Inactive:        59468 kB
HighTotal:      131008 kB
HighFree:        55440 kB
LowTotal:       903652 kB
LowFree:        854352 kB
SwapTotal:     2097136 kB
SwapFree:      2096972 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            10620 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:47:24 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 518 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1071 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =====
c   -- Clauses(.)/Splits(s): .........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1065     6934 |     355       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 300[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:69860     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   85971   205224 |   28657       0        0     nan |  0.000 % |
c |       100 |   84914   203008 |   31522      68      453     6.7 |  1.041 % |
c |       250 |   84059   201168 |   34674     199     1521     7.6 |  1.894 % |
c |       475 |   82900   198609 |   38142     380     2806     7.4 |  3.111 % |
c |       813 |   81889   196392 |   41956     698     5285     7.6 |  4.161 % |
c |      1319 |   81408   195320 |   46152    1186     9049     7.6 |  4.676 % |
c |      2078 |   80971   194353 |   50767    1919    17740     9.2 |  5.135 % |
c |      3219 |   80629   193601 |   55844    3013    32516    10.8 |  5.489 % |
c |      4927 |   80341   192960 |   61428    4679    49894    10.7 |  5.797 % |
c |      7489 |   80213   192665 |   67571    7222    97618    13.5 |  5.942 % |
c |     11333 |   80093   192392 |   74328   11047   174199    15.8 |  6.071 % |
c |     17099 |   79990   192155 |   81761   16787   418802    24.9 |  6.188 % |
c |     25748 |   79929   192022 |   89937   25430   636257    25.0 |  6.247 % |
c ==============================================================================
c [1mFound solution: 292[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 |     33905 |   79903   191991 |   26634   33577  1065587    31.7 |  6.247 % |
c |     34005 |   79903   191991 |   29297   15046   541258    36.0 |  6.406 % |
c |     34155 |   79859   191887 |   32227   15195   543422    35.8 |  6.459 % |
c |     34380 |   79859   191887 |   35449   15420   546677    35.5 |  6.459 % |
c |     34718 |   79859   191887 |   38994   15758   555807    35.3 |  6.459 % |
c |     35224 |   79859   191887 |   42894   16264   563462    34.6 |  6.459 % |
c |     35983 |   79859   191887 |   47183   17023   599538    35.2 |  6.459 % |
c |     37122 |   79859   191887 |   51902   18162   627006    34.5 |  6.459 % |
c |     38830 |   79859   191887 |   57092   19870   672608    33.9 |  6.459 % |
c |     41392 |   79859   191887 |   62801   22432   741323    33.0 |  6.459 % |
c |     45237 |   79770   191690 |   69081   26268   854128    32.5 |  6.553 % |
c |     51006 |   79731   191597 |   75989   32035  1028474    32.1 |  6.600 % |
c |     59656 |   79731   191597 |   83588   40685  1759365    43.2 |  6.600 % |
c |     72631 |   79731   191597 |   91947   53660  2294813    42.8 |  6.600 % |
c |     92092 |   79731   191597 |  101142   73121  4025752    55.1 |  6.600 % |
c |    121285 |   79731   191597 |  111256  102314  7080579    69.2 |  6.600 % |
c |    165074 |   79647   191407 |  122382   48578  2432119    50.1 |  6.692 % |
c |    230758 |   79504   191083 |  134620  114250  7725415    67.6 |  6.849 % |
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 -#### 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.84 0.94 0.90 2/54 27610
Raw data (stat): 27610 (runsolver) R 27609 25347 25346 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420611314 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 4657 0 0 0 986 12 0 0 25 0 1 0 420611314 21635072 4442 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5282 4442 603 41 0 5241 0
vsize: 21128
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 4763 0 0 0 1985 13 0 0 25 0 1 0 420611314 22175744 4548 4294967295 134512640 134672761 3221224624 3221223792 134553595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5414 4548 603 41 0 5373 0
vsize: 21656
[startup+30.0004 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 4937 0 0 0 2983 14 0 0 25 0 1 0 420611314 22859776 4722 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5581 4722 603 41 0 5540 0
vsize: 22324
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 5262 0 0 0 3983 15 0 0 25 0 1 0 420611314 24252416 5047 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5921 5047 603 41 0 5880 0
vsize: 23684
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 5415 0 0 0 4983 15 0 0 25 0 1 0 420611314 24793088 5200 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6053 5200 603 41 0 6012 0
vsize: 24212
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 5604 0 0 0 5982 16 0 0 25 0 1 0 420611314 25604096 5389 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6251 5389 603 41 0 6210 0
vsize: 25004
[startup+70.002 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 5760 0 0 0 6982 17 0 0 25 0 1 0 420611314 26144768 5545 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6383 5545 603 41 0 6342 0
vsize: 25532
[startup+80.0026 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 5979 0 0 0 7981 17 0 0 25 0 1 0 420611314 27213824 5764 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6644 5764 603 41 0 6603 0
vsize: 26576
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6185 0 0 0 8981 18 0 0 25 0 1 0 420611314 28356608 5970 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6923 5970 603 41 0 6882 0
vsize: 27692
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6185 0 0 0 9981 18 0 0 25 0 1 0 420611314 28356608 5970 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6923 5970 603 41 0 6882 0
vsize: 27692
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6185 0 0 0 10981 18 0 0 25 0 1 0 420611314 28356608 5970 4294967295 134512640 134672761 3221224624 3221223792 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6923 5970 603 41 0 6882 0
vsize: 27692
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6261 0 0 0 11981 18 0 0 25 0 1 0 420611314 28622848 6046 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6988 6046 603 41 0 6947 0
vsize: 27952
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6401 0 0 0 12980 19 0 0 25 0 1 0 420611314 29163520 6186 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7120 6186 603 41 0 7079 0
vsize: 28480
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6603 0 0 0 13980 19 0 0 25 0 1 0 420611314 29962240 6388 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7315 6388 603 41 0 7274 0
vsize: 29260
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 6853 0 0 0 14980 20 0 0 25 0 1 0 420611314 31039488 6638 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7578 6638 603 41 0 7537 0
vsize: 30312
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 7053 0 0 0 15980 20 0 0 25 0 1 0 420611314 31842304 6838 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7774 6838 603 41 0 7733 0
vsize: 31096
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 7403 0 0 0 16979 21 0 0 25 0 1 0 420611314 33177600 7188 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8100 7188 603 41 0 8059 0
vsize: 32400
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 7617 0 0 0 17978 22 0 0 25 0 1 0 420611314 34115584 7402 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8329 7402 603 41 0 8288 0
vsize: 33316
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 7892 0 0 0 18978 22 0 0 25 0 1 0 420611314 35176448 7677 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8588 7677 603 41 0 8547 0
vsize: 34352
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 8268 0 0 0 19977 24 0 0 25 0 1 0 420611314 36786176 8053 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8981 8053 603 41 0 8940 0
vsize: 35924
[startup+210.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 8645 0 0 0 20976 25 0 0 25 0 1 0 420611314 38252544 8430 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9339 8430 603 41 0 9298 0
vsize: 37356
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 8964 0 0 0 21975 26 0 0 25 0 1 0 420611314 39845888 8749 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9728 8749 603 41 0 9687 0
vsize: 38912
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 9284 0 0 0 22974 27 0 0 25 0 1 0 420611314 41193472 9069 4294967295 134512640 134672761 3221224624 3221223552 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10057 9069 603 41 0 10016 0
vsize: 40228
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 9521 0 0 0 23973 28 0 0 25 0 1 0 420611314 42127360 9306 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10285 9306 603 41 0 10244 0
vsize: 41140
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 9677 0 0 0 24972 29 0 0 25 0 1 0 420611314 42668032 9462 4294967295 134512640 134672761 3221224624 3221223808 134558513 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10417 9462 603 41 0 10376 0
vsize: 41668
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 9872 0 0 0 25970 30 0 0 25 0 1 0 420611314 43470848 9657 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10613 9657 603 41 0 10572 0
vsize: 42452
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 10088 0 0 0 26970 31 0 0 25 0 1 0 420611314 44417024 9873 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10844 9873 603 41 0 10803 0
vsize: 43376
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 10348 0 0 0 27970 31 0 0 25 0 1 0 420611314 45486080 10133 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11105 10133 603 41 0 11064 0
vsize: 44420
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 10570 0 0 0 28969 32 0 0 25 0 1 0 420611314 46288896 10355 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11301 10355 603 41 0 11260 0
vsize: 45204
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 10778 0 0 0 29969 33 0 0 25 0 1 0 420611314 47230976 10563 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11531 10563 603 41 0 11490 0
vsize: 46124
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 11022 0 0 0 30967 34 0 0 25 0 1 0 420611314 48168960 10807 4294967295 134512640 134672761 3221224624 3221223768 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11760 10807 603 41 0 11719 0
vsize: 47040
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 11265 0 0 0 31967 35 0 0 25 0 1 0 420611314 49115136 11050 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11991 11050 603 41 0 11950 0
vsize: 47964
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 11592 0 0 0 32965 37 0 0 25 0 1 0 420611314 50462720 11377 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12320 11377 603 41 0 12279 0
vsize: 49280
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 11968 0 0 0 33965 38 0 0 25 0 1 0 420611314 52064256 11753 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12711 11753 603 41 0 12670 0
vsize: 50844
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 12267 0 0 0 34964 39 0 0 25 0 1 0 420611314 53280768 12052 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13008 12052 603 41 0 12967 0
vsize: 52032
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 12539 0 0 0 35964 39 0 0 25 0 1 0 420611314 54358016 12324 4294967295 134512640 134672761 3221224624 3221223760 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13271 12324 603 41 0 13230 0
vsize: 53084
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 12786 0 0 0 36963 40 0 0 25 0 1 0 420611314 55304192 12571 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13502 12571 603 41 0 13461 0
vsize: 54008
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13026 0 0 0 37962 41 0 0 25 0 1 0 420611314 56385536 12811 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13766 12811 603 41 0 13725 0
vsize: 55064
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13292 0 0 0 38961 42 0 0 25 0 1 0 420611314 57450496 13077 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14026 13077 603 41 0 13985 0
vsize: 56104
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13465 0 0 0 39961 43 0 0 25 0 1 0 420611314 58126336 13250 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14191 13250 603 41 0 14150 0
vsize: 56764
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13627 0 0 0 40960 43 0 0 25 0 1 0 420611314 58802176 13412 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14356 13412 603 41 0 14315 0
vsize: 57424
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13795 0 0 0 41960 44 0 0 25 0 1 0 420611314 59469824 13580 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 13580 603 41 0 14478 0
vsize: 58076
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 42960 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 43960 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 44960 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 45960 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 46960 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 47961 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 48961 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 49961 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 50961 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 51961 44 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 52960 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 53959 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 54958 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 55958 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 56959 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 57959 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 58959 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 59959 45 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 60959 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+620.011 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 61960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+630.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 62960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+640.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 63960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223824 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+650.011 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 64960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+660.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 65960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+670.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 66960 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+680.01 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 67961 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+690.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 68961 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+700.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 69961 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+710.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 70961 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+720.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 71961 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+730.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 72962 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223824 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+740.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 73962 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+750.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 13864 0 0 0 74962 46 0 0 25 0 1 0 420611314 59740160 13649 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14585 13649 603 41 0 14544 0
vsize: 58340
[startup+760.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 14033 0 0 0 75962 46 0 0 25 0 1 0 420611314 60411904 13818 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14749 13818 603 41 0 14708 0
vsize: 58996
[startup+770.011 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 14185 0 0 0 76960 47 0 0 25 0 1 0 420611314 61087744 13970 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14914 13970 603 41 0 14873 0
vsize: 59656
[startup+780.011 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 14336 0 0 0 77960 48 0 0 25 0 1 0 420611314 61632512 14121 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15047 14121 603 41 0 15006 0
vsize: 60188
[startup+790.011 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 14594 0 0 0 78959 48 0 0 25 0 1 0 420611314 62709760 14379 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15310 14379 603 41 0 15269 0
vsize: 61240
[startup+800.011 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 14847 0 0 0 79959 49 0 0 25 0 1 0 420611314 63643648 14632 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15538 14632 603 41 0 15497 0
vsize: 62152
[startup+810.012 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 15184 0 0 0 80958 50 0 0 25 0 1 0 420611314 65126400 14969 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15900 14969 603 41 0 15859 0
vsize: 63600
[startup+820.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 15518 0 0 0 81957 51 0 0 25 0 1 0 420611314 66473984 15303 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16229 15303 603 41 0 16188 0
vsize: 64916
[startup+830.012 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 15873 0 0 0 82957 52 0 0 25 0 1 0 420611314 67956736 15658 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16591 15658 603 41 0 16550 0
vsize: 66364
[startup+840.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 16242 0 0 0 83956 52 0 0 25 0 1 0 420611314 69435392 16027 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16952 16027 603 41 0 16911 0
vsize: 67808
[startup+850.012 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 16580 0 0 0 84955 54 0 0 25 0 1 0 420611314 70795264 16365 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17284 16365 603 41 0 17243 0
vsize: 69136
[startup+860.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 16980 0 0 0 85955 54 0 0 25 0 1 0 420611314 72929280 16765 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17805 16765 603 41 0 17764 0
vsize: 71220
[startup+870.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 17395 0 0 0 86954 55 0 0 25 0 1 0 420611314 74678272 17180 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18232 17180 603 41 0 18191 0
vsize: 72928
[startup+880.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 17766 0 0 0 87953 56 0 0 25 0 1 0 420611314 76148736 17551 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18591 17551 603 41 0 18550 0
vsize: 74364
[startup+890.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 18152 0 0 0 88952 57 0 0 25 0 1 0 420611314 77766656 17937 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18986 17937 603 41 0 18945 0
vsize: 75944
[startup+900.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 18512 0 0 0 89951 58 0 0 25 0 1 0 420611314 79241216 18297 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19346 18297 603 41 0 19305 0
vsize: 77384
[startup+910.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 18860 0 0 0 90951 59 0 0 25 0 1 0 420611314 80601088 18645 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19678 18645 603 41 0 19637 0
vsize: 78712
[startup+920.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 19186 0 0 0 91950 60 0 0 25 0 1 0 420611314 81944576 18971 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20006 18971 603 41 0 19965 0
vsize: 80024
[startup+930.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 19535 0 0 0 92949 61 0 0 25 0 1 0 420611314 83431424 19320 4294967295 134512640 134672761 3221224624 3221223728 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20369 19320 603 41 0 20328 0
vsize: 81476
[startup+940.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 19920 0 0 0 93949 62 0 0 25 0 1 0 420611314 84910080 19705 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20730 19705 603 41 0 20689 0
vsize: 82920
[startup+950.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 20318 0 0 0 94948 63 0 0 25 0 1 0 420611314 86528000 20103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21125 20103 603 41 0 21084 0
vsize: 84500
[startup+960.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 20753 0 0 0 95947 64 0 0 25 0 1 0 420611314 88428544 20538 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21589 20538 603 41 0 21548 0
vsize: 86356
[startup+970.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21050 0 0 0 96947 64 0 0 25 0 1 0 420611314 89640960 20835 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21885 20835 603 41 0 21844 0
vsize: 87540
[startup+980.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 97946 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221221664 134565798 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+990.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 98946 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 99946 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 100946 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 101947 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223792 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 102947 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223760 134560657 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 103947 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21333 0 0 0 104947 65 0 0 25 0 1 0 420611314 90718208 21118 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21118 603 41 0 22107 0
vsize: 88592
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21334 0 0 0 105947 65 0 0 25 0 1 0 420611314 90718208 21119 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21119 603 41 0 22107 0
vsize: 88592
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21334 0 0 0 106948 65 0 0 25 0 1 0 420611314 90718208 21119 4294967295 134512640 134672761 3221224624 3221223728 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21119 603 41 0 22107 0
vsize: 88592
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21334 0 0 0 107948 65 0 0 25 0 1 0 420611314 90718208 21119 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21119 603 41 0 22107 0
vsize: 88592
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21334 0 0 0 108948 65 0 0 25 0 1 0 420611314 90718208 21119 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21119 603 41 0 22107 0
vsize: 88592
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 109948 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 110948 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 111949 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 112949 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 113949 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 114949 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 115949 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223728 134555211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 116950 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223728 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 117950 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 118950 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223716 134555596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 27610
Raw data (stat): 27610 (minisat+) R 27609 25347 25346 0 -1 0 21336 0 0 0 119950 65 0 0 25 0 1 0 420611314 90718208 21121 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22148 21121 603 41 0 22107 0
vsize: 88592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 27610
Raw data (stat): 27610 (minisat+) Z 27609 25347 25346 0 -1 12 21339 0 0 0 119950 69 0 0 25 0 1 0 420611314 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.51
CPU system time (s): 0.699893
CPU usage (%): 100.012
Max. virtual memory (Kb): 88592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####