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-ii32d2.opb
MD5SUM	a483fc3761bb4050329265bf3a3a7ca5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	372
Optimality of the best value was proved	NO
Number of terms in the objective function	808
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	808
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	808
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04284
Number of variables	808
Total number of constraints	5557
Number of constraints which are clauses	5557
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	32
Trace number 4915

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        907048 kB
Buffers:         34064 kB
Cached:          57416 kB
SwapCached:        320 kB
Active:          49512 kB
Inactive:        45200 kB
HighTotal:      131008 kB
HighFree:        69552 kB
LowTotal:       903652 kB
LowFree:        837496 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27308 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:08:57 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 1400 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 5557 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 |    5557    18748 |    1852       0        0     nan |  0.000 % |
c |       100 |    5557    18748 |    2037     100     8211    82.1 |  0.006 % |
c |       252 |    5557    18748 |    2240     252    19966    79.2 |  0.000 % |
c |       477 |    5557    18748 |    2465     477    34035    71.4 |  0.000 % |
c |       816 |    5557    18748 |    2711     816    61162    75.0 |  0.000 % |
c |      1322 |    5557    18748 |    2982    1322   101974    77.1 |  0.000 % |
c |      2082 |    5557    18748 |    3280    2082   175391    84.2 |  0.000 % |
c |      3222 |    5557    18748 |    3609    3222   287281    89.2 |  0.000 % |
c |      4930 |    5557    18748 |    3969    3034   259982    85.7 |  0.000 % |
c |      7492 |    5557    18748 |    4366    3524   289629    82.2 |  0.000 % |
c ==============================================================================
c [1mFound solution: 386[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:37286     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8400 |   50849   124642 |   16949    4432   356590    80.5 |  0.000 % |
c |      8500 |   50849   124642 |   18643    4532   364865    80.5 |  0.033 % |
c |      8650 |   50849   124642 |   20508    4682   378388    80.8 |  0.033 % |
c |      8875 |   50835   124614 |   22559    4906   393775    80.3 |  0.055 % |
c |      9214 |   50835   124614 |   24815    5245   423878    80.8 |  0.055 % |
c |      9720 |   50835   124614 |   27296    5751   464928    80.8 |  0.055 % |
c |     10479 |   50835   124614 |   30026    6510   536138    82.4 |  0.055 % |
c |     11619 |   50835   124614 |   33028    7650   644338    84.2 |  0.055 % |
c |     13328 |   50835   124614 |   36331    9359   803264    85.8 |  0.055 % |
c |     15892 |   50835   124614 |   39964   11923  1011917    84.9 |  0.055 % |
c |     19736 |   50819   124582 |   43961   15766  1313225    83.3 |  0.081 % |
c |     25502 |   50819   124582 |   48357   21532  1829113    84.9 |  0.081 % |
c |     34154 |   50496   123909 |   53193   30138  2562415    85.0 |  0.650 % |
c |     47129 |   50477   123870 |   58512   43112  3694785    85.7 |  0.683 % |
c |     66590 |   50370   123647 |   64363   19893  1410152    70.9 |  0.871 % |
c ==============================================================================
c [1mFound solution: 374[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 |     72696 |   49782   122492 |   16594   25929  1997415    77.0 |  0.871 % |
c |     72798 |   49745   122413 |   18253   13066   980835    75.1 |  2.403 % |
c |     72948 |   49745   122413 |   20078   13216   995146    75.3 |  2.403 % |
c |     73175 |   49745   122413 |   22086   13443  1023685    76.2 |  2.403 % |
c |     73514 |   49715   122349 |   24295   13781  1055470    76.6 |  2.455 % |
c |     74020 |   49715   122349 |   26724   14287  1097966    76.9 |  2.455 % |
c |     74780 |   49679   122273 |   29397   15046  1160728    77.1 |  2.520 % |
c |     75921 |   49640   122190 |   32337   16186  1244649    76.9 |  2.591 % |
c ==============================================================================
c [1mFound solution: 373[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 |     76756 |   49684   122335 |   16561   17021  1322203    77.7 |  2.591 % |
c |     76856 |   47021   116453 |   18217   17038  1322673    77.6 |  7.739 % |
c |     77006 |   46205   114637 |   20038   17161  1328197    77.4 |  9.357 % |
c |     77231 |   46205   114637 |   22042   17386  1343048    77.2 |  9.357 % |
c |     77569 |   46205   114637 |   24246   17724  1365837    77.1 |  9.357 % |
c |     78078 |   46151   114515 |   26671   18232  1404045    77.0 |  9.467 % |
c |     78840 |   46101   114405 |   29338   18993  1463530    77.1 |  9.564 % |
c |     79981 |   46043   114277 |   32272   20132  1550128    77.0 |  9.677 % |
c |     81689 |   46043   114277 |   35499   21840  1673169    76.6 |  9.677 % |
c |     84252 |   45935   114043 |   39049   24396  1851087    75.9 |  9.881 % |
c |     88099 |   45891   113943 |   42954   28242  2169099    76.8 |  9.972 % |
c |     93868 |   45833   113813 |   47250   34008  2666510    78.4 | 10.088 % |
c |    102517 |   45519   113123 |   51975   42638  3411087    80.0 | 10.697 % |
c ==============================================================================
c [1mFound solution: 372[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 |    115430 |   44752   111423 |   14917   55429  4585559    82.7 | 10.697 % |
c |    115531 |   44685   111278 |   16408   16626  1236706    74.4 | 12.317 % |
c |    115681 |   44643   111190 |   18049   16617  1236062    74.4 | 12.391 % |
c |    115906 |   44643   111190 |   19854   16842  1249766    74.2 | 12.391 % |
c |    116243 |   44643   111190 |   21839   17179  1266518    73.7 | 12.391 % |
c |    116749 |   44643   111190 |   24023   17685  1298014    73.4 | 12.391 % |
c |    117509 |   44586   111061 |   26426   18444  1346422    73.0 | 12.508 % |
c |    118648 |   44586   111061 |   29069   19583  1427861    72.9 | 12.508 % |
c |    120356 |   44586   111061 |   31975   21291  1567161    73.6 | 12.508 % |
c |    122918 |   44586   111061 |   35173   23853  1778453    74.6 | 12.508 % |
c |    126762 |   44586   111061 |   38690   27697  2063517    74.5 | 12.508 % |
c |    132528 |   44586   111061 |   42559   33463  2536232    75.8 | 12.508 % |
c |    141177 |   44353   110536 |   46815   42106  3294557    78.2 | 12.980 % |
c |    154151 |   44113   110002 |   51497   20387  1050521    51.5 | 13.456 % |
c |    173612 |   43984   109719 |   56647   39845  2733175    68.6 | 13.705 % |
c |    202804 |   43797   109306 |   62312   25456  1873780    73.6 | 14.070 % |
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 -x745 x746 -x747 x748 x749 -x750 -x751 x7#### 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.83 0.92 0.90 2/55 23189
Raw data (stat): 23189 (runsolver) R 23188 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478947405 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0018 s]
Raw data (loadavg): 0.85 0.92 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 3275 0 0 0 990 7 0 0 25 0 1 0 478947405 15482880 3194 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3780 3194 603 41 0 3739 0
vsize: 15120
[startup+20.0021 s]
Raw data (loadavg): 0.88 0.92 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 3671 0 0 0 1989 9 0 0 25 0 1 0 478947405 17010688 3590 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3590 603 41 0 4112 0
vsize: 16612
[startup+30.0028 s]
Raw data (loadavg): 0.89 0.92 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 4000 0 0 0 2988 10 0 0 25 0 1 0 478947405 18354176 3919 4294967295 134512640 134672761 3221224640 3221223840 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4481 3919 603 41 0 4440 0
vsize: 17924
[startup+40.0032 s]
Raw data (loadavg): 0.91 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 4259 0 0 0 3987 11 0 0 25 0 1 0 478947405 19431424 4178 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4744 4178 603 41 0 4703 0
vsize: 18976
[startup+50.0039 s]
Raw data (loadavg): 0.92 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 4487 0 0 0 4986 12 0 0 25 0 1 0 478947405 20549632 4406 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5017 4406 603 41 0 4976 0
vsize: 20068
[startup+60.0051 s]
Raw data (loadavg): 0.93 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 4693 0 0 0 5986 12 0 0 25 0 1 0 478947405 21356544 4612 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5214 4612 603 41 0 5173 0
vsize: 20856
[startup+70.0063 s]
Raw data (loadavg): 0.94 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 4880 0 0 0 6986 13 0 0 25 0 1 0 478947405 22159360 4799 4294967295 134512640 134672761 3221224640 3221223824 134559522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5410 4799 603 41 0 5369 0
vsize: 21640
[startup+80.0067 s]
Raw data (loadavg): 0.95 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 5156 0 0 0 7983 15 0 0 25 0 1 0 478947405 23252992 5075 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5677 5075 603 41 0 5636 0
vsize: 22708
[startup+90.0072 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 5414 0 0 0 8982 16 0 0 25 0 1 0 478947405 24387584 5333 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5333 603 41 0 5913 0
vsize: 23816
[startup+100.008 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 5597 0 0 0 9981 16 0 0 25 0 1 0 478947405 25055232 5516 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6117 5516 603 41 0 6076 0
vsize: 24468
[startup+110.009 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 5769 0 0 0 10980 18 0 0 25 0 1 0 478947405 25726976 5688 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6281 5688 603 41 0 6240 0
vsize: 25124
[startup+120.009 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 5962 0 0 0 11980 19 0 0 25 0 1 0 478947405 26570752 5881 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6487 5881 603 41 0 6446 0
vsize: 25948
[startup+130.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6155 0 0 0 12979 19 0 0 25 0 1 0 478947405 27459584 6074 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6704 6074 603 41 0 6663 0
vsize: 26816
[startup+140.01 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6303 0 0 0 13979 20 0 0 25 0 1 0 478947405 28270592 6222 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 6222 603 41 0 6861 0
vsize: 27608
[startup+150.011 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6445 0 0 0 14978 21 0 0 25 0 1 0 478947405 28807168 6364 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7033 6364 603 41 0 6992 0
vsize: 28132
[startup+160.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6570 0 0 0 15979 21 0 0 25 0 1 0 478947405 29347840 6489 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7165 6489 603 41 0 7124 0
vsize: 28660
[startup+170.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23189
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6726 0 0 0 16978 21 0 0 25 0 1 0 478947405 30060544 6645 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7339 6645 603 41 0 7298 0
vsize: 29356
[startup+180.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 6900 0 0 0 17978 21 0 0 25 0 1 0 478947405 30769152 6819 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7512 6819 603 41 0 7471 0
vsize: 30048
[startup+190.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7045 0 0 0 18977 22 0 0 25 0 1 0 478947405 31449088 6964 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7678 6964 603 41 0 7637 0
vsize: 30712
[startup+200.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7238 0 0 0 19977 23 0 0 25 0 1 0 478947405 32292864 7157 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7884 7157 603 41 0 7843 0
vsize: 31536
[startup+210.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7377 0 0 0 20976 24 0 0 25 0 1 0 478947405 32870400 7296 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8025 7296 603 41 0 7984 0
vsize: 32100
[startup+220.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7526 0 0 0 21976 24 0 0 25 0 1 0 478947405 33443840 7445 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8165 7445 603 41 0 8124 0
vsize: 32660
[startup+230.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7710 0 0 0 22976 25 0 0 25 0 1 0 478947405 34336768 7629 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8383 7629 603 41 0 8342 0
vsize: 33532
[startup+240.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 7896 0 0 0 23976 25 0 0 25 0 1 0 478947405 35123200 7815 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8575 7815 603 41 0 8534 0
vsize: 34300
[startup+250.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8021 0 0 0 24976 25 0 0 25 0 1 0 478947405 35692544 7940 4294967295 134512640 134672761 3221224640 3221223808 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8714 7940 603 41 0 8673 0
vsize: 34856
[startup+260.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8113 0 0 0 25975 26 0 0 25 0 1 0 478947405 35962880 8032 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8780 8032 603 41 0 8739 0
vsize: 35120
[startup+270.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8214 0 0 0 26975 27 0 0 25 0 1 0 478947405 36372480 8133 4294967295 134512640 134672761 3221224640 3221223808 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8880 8133 603 41 0 8839 0
vsize: 35520
[startup+280.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8357 0 0 0 27975 27 0 0 25 0 1 0 478947405 37044224 8276 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9044 8276 603 41 0 9003 0
vsize: 36176
[startup+290.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8497 0 0 0 28974 28 0 0 25 0 1 0 478947405 37625856 8416 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9186 8416 603 41 0 9145 0
vsize: 36744
[startup+300.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8634 0 0 0 29974 28 0 0 25 0 1 0 478947405 38182912 8553 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9322 8553 603 41 0 9281 0
vsize: 37288
[startup+310.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8772 0 0 0 30973 29 0 0 25 0 1 0 478947405 38883328 8691 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9493 8691 603 41 0 9452 0
vsize: 37972
[startup+320.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8895 0 0 0 31973 30 0 0 25 0 1 0 478947405 39383040 8814 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9615 8814 603 41 0 9574 0
vsize: 38460
[startup+330.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 8977 0 0 0 32973 30 0 0 25 0 1 0 478947405 39784448 8896 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9713 8896 603 41 0 9672 0
vsize: 38852
[startup+340.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9079 0 0 0 33973 30 0 0 25 0 1 0 478947405 40226816 8998 4294967295 134512640 134672761 3221224640 3221223808 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 8998 603 41 0 9780 0
vsize: 39284
[startup+350.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9088 0 0 0 34973 30 0 0 25 0 1 0 478947405 40226816 9007 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 9007 603 41 0 9780 0
vsize: 39284
[startup+360.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9088 0 0 0 35973 30 0 0 25 0 1 0 478947405 40226816 9007 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9821 9007 603 41 0 9780 0
vsize: 39284
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9096 0 0 0 36972 31 0 0 25 0 1 0 478947405 40226816 9015 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9821 9015 603 41 0 9780 0
vsize: 39284
[startup+380.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9113 0 0 0 37972 31 0 0 25 0 1 0 478947405 40361984 9032 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9854 9032 603 41 0 9813 0
vsize: 39416
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9167 0 0 0 38972 31 0 0 25 0 1 0 478947405 40722432 9086 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9086 603 41 0 9901 0
vsize: 39768
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9169 0 0 0 39973 31 0 0 25 0 1 0 478947405 40722432 9088 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9088 603 41 0 9901 0
vsize: 39768
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9170 0 0 0 40973 31 0 0 25 0 1 0 478947405 40722432 9089 4294967295 134512640 134672761 3221224640 3221223812 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9089 603 41 0 9901 0
vsize: 39768
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9170 0 0 0 41973 31 0 0 25 0 1 0 478947405 40722432 9089 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9089 603 41 0 9901 0
vsize: 39768
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9170 0 0 0 42973 31 0 0 25 0 1 0 478947405 40722432 9089 4294967295 134512640 134672761 3221224640 3221223812 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9089 603 41 0 9901 0
vsize: 39768
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9182 0 0 0 43973 32 0 0 25 0 1 0 478947405 40722432 9101 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9101 603 41 0 9901 0
vsize: 39768
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9183 0 0 0 44973 32 0 0 25 0 1 0 478947405 40722432 9102 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9102 603 41 0 9901 0
vsize: 39768
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9183 0 0 0 45973 32 0 0 25 0 1 0 478947405 40722432 9102 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9102 603 41 0 9901 0
vsize: 39768
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23191
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9188 0 0 0 46973 32 0 0 25 0 1 0 478947405 40886272 9107 4294967295 134512640 134672761 3221224640 3221223808 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9982 9107 603 41 0 9941 0
vsize: 39928
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9189 0 0 0 47974 32 0 0 25 0 1 0 478947405 40886272 9108 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9982 9108 603 41 0 9941 0
vsize: 39928
[startup+490.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9189 0 0 0 48974 32 0 0 25 0 1 0 478947405 40886272 9108 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9982 9108 603 41 0 9941 0
vsize: 39928
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9212 0 0 0 49974 32 0 0 25 0 1 0 478947405 40886272 9131 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9982 9131 603 41 0 9941 0
vsize: 39928
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9220 0 0 0 50974 32 0 0 25 0 1 0 478947405 41050112 9139 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10022 9139 603 41 0 9981 0
vsize: 40088
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9228 0 0 0 51974 32 0 0 25 0 1 0 478947405 41050112 9147 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10022 9147 603 41 0 9981 0
vsize: 40088
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9236 0 0 0 52974 32 0 0 25 0 1 0 478947405 41050112 9155 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10022 9155 603 41 0 9981 0
vsize: 40088
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9270 0 0 0 53974 32 0 0 25 0 1 0 478947405 41213952 9189 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10062 9189 603 41 0 10021 0
vsize: 40248
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9270 0 0 0 54974 32 0 0 25 0 1 0 478947405 41213952 9189 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10062 9189 603 41 0 10021 0
vsize: 40248
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9278 0 0 0 55974 32 0 0 25 0 1 0 478947405 41213952 9197 4294967295 134512640 134672761 3221224640 3221223840 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10062 9197 603 41 0 10021 0
vsize: 40248
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9284 0 0 0 56975 32 0 0 25 0 1 0 478947405 41377792 9203 4294967295 134512640 134672761 3221224640 3221223808 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10102 9203 603 41 0 10061 0
vsize: 40408
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9317 0 0 0 57974 33 0 0 25 0 1 0 478947405 41574400 9236 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9236 603 41 0 10109 0
vsize: 40600
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 58975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 59975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 60975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 61975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 62975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 63975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 64976 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 23193
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 65976 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+670.032 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 23197
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 66975 33 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+680.032 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 67971 37 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+690.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9319 0 0 0 68971 37 0 0 25 0 1 0 478947405 41574400 9238 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9238 603 41 0 10109 0
vsize: 40600
[startup+700.033 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9329 0 0 0 69971 37 0 0 25 0 1 0 478947405 41574400 9248 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9248 603 41 0 10109 0
vsize: 40600
[startup+710.033 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9338 0 0 0 70971 37 0 0 25 0 1 0 478947405 41574400 9257 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9257 603 41 0 10109 0
vsize: 40600
[startup+720.033 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9340 0 0 0 71971 37 0 0 25 0 1 0 478947405 41574400 9259 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9259 603 41 0 10109 0
vsize: 40600
[startup+730.033 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 23246
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9345 0 0 0 72972 37 0 0 25 0 1 0 478947405 41574400 9264 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9264 603 41 0 10109 0
vsize: 40600
[startup+740.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 23248
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9345 0 0 0 73972 38 0 0 25 0 1 0 478947405 41574400 9264 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9264 603 41 0 10109 0
vsize: 40600
[startup+750.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 23248
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9347 0 0 0 74972 38 0 0 25 0 1 0 478947405 41574400 9266 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9266 603 41 0 10109 0
vsize: 40600
[startup+760.034 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 23248
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9347 0 0 0 75972 38 0 0 25 0 1 0 478947405 41574400 9266 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9266 603 41 0 10109 0
vsize: 40600
[startup+770.034 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 23248
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9347 0 0 0 76972 38 0 0 25 0 1 0 478947405 41574400 9266 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9266 603 41 0 10109 0
vsize: 40600
[startup+780.034 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9347 0 0 0 77972 38 0 0 25 0 1 0 478947405 41574400 9266 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10150 9266 603 41 0 10109 0
vsize: 40600
[startup+790.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9356 0 0 0 78973 38 0 0 25 0 1 0 478947405 41771008 9275 4294967295 134512640 134672761 3221224640 3221223808 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9275 603 41 0 10157 0
vsize: 40792
[startup+800.034 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 79973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+810.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 80973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+820.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 81973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+830.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 82973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+840.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 83973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223744 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+850.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 84973 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+860.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 85974 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+870.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 86974 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9366 0 0 0 87974 38 0 0 25 0 1 0 478947405 41771008 9285 4294967295 134512640 134672761 3221224640 3221223776 134565134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9285 603 41 0 10157 0
vsize: 40792
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9371 0 0 0 88974 38 0 0 25 0 1 0 478947405 41771008 9290 4294967295 134512640 134672761 3221224640 3221223808 134561275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9290 603 41 0 10157 0
vsize: 40792
[startup+900.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9372 0 0 0 89974 38 0 0 25 0 1 0 478947405 41771008 9291 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9291 603 41 0 10157 0
vsize: 40792
[startup+910.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9373 0 0 0 90974 38 0 0 25 0 1 0 478947405 41771008 9292 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9292 603 41 0 10157 0
vsize: 40792
[startup+920.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9373 0 0 0 91974 38 0 0 25 0 1 0 478947405 41771008 9292 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9292 603 41 0 10157 0
vsize: 40792
[startup+930.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9378 0 0 0 92974 38 0 0 25 0 1 0 478947405 41771008 9297 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9297 603 41 0 10157 0
vsize: 40792
[startup+940.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9378 0 0 0 93975 38 0 0 25 0 1 0 478947405 41771008 9297 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9297 603 41 0 10157 0
vsize: 40792
[startup+950.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9380 0 0 0 94975 38 0 0 25 0 1 0 478947405 41771008 9299 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10198 9299 603 41 0 10157 0
vsize: 40792
[startup+960.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9392 0 0 0 95975 38 0 0 25 0 1 0 478947405 41934848 9311 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10238 9311 603 41 0 10197 0
vsize: 40952
[startup+970.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9397 0 0 0 96975 38 0 0 25 0 1 0 478947405 41934848 9316 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10238 9316 603 41 0 10197 0
vsize: 40952
[startup+980.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9428 0 0 0 97975 38 0 0 25 0 1 0 478947405 42131456 9347 4294967295 134512640 134672761 3221224640 3221223808 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9347 603 41 0 10245 0
vsize: 41144
[startup+990.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9431 0 0 0 98975 38 0 0 25 0 1 0 478947405 42131456 9350 4294967295 134512640 134672761 3221224640 3221223808 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9350 603 41 0 10245 0
vsize: 41144
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9432 0 0 0 99975 38 0 0 25 0 1 0 478947405 42131456 9351 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9351 603 41 0 10245 0
vsize: 41144
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23250
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9432 0 0 0 100976 38 0 0 25 0 1 0 478947405 42131456 9351 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9351 603 41 0 10245 0
vsize: 41144
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9432 0 0 0 101976 38 0 0 25 0 1 0 478947405 42131456 9351 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10286 9351 603 41 0 10245 0
vsize: 41144
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9432 0 0 0 102975 39 0 0 25 0 1 0 478947405 42131456 9351 4294967295 134512640 134672761 3221224640 3221223808 134560864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9351 603 41 0 10245 0
vsize: 41144
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9432 0 0 0 103975 39 0 0 25 0 1 0 478947405 42131456 9351 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9351 603 41 0 10245 0
vsize: 41144
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9438 0 0 0 104976 39 0 0 25 0 1 0 478947405 42131456 9357 4294967295 134512640 134672761 3221224640 3221223808 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10286 9357 603 41 0 10245 0
vsize: 41144
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9448 0 0 0 105976 39 0 0 25 0 1 0 478947405 42295296 9367 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9367 603 41 0 10285 0
vsize: 41304
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23252
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9449 0 0 0 106976 39 0 0 25 0 1 0 478947405 42295296 9368 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9368 603 41 0 10285 0
vsize: 41304
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9454 0 0 0 107976 39 0 0 25 0 1 0 478947405 42295296 9373 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9373 603 41 0 10285 0
vsize: 41304
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9467 0 0 0 108976 39 0 0 25 0 1 0 478947405 42295296 9386 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9386 603 41 0 10285 0
vsize: 41304
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9468 0 0 0 109976 39 0 0 25 0 1 0 478947405 42295296 9387 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9387 603 41 0 10285 0
vsize: 41304
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9469 0 0 0 110976 39 0 0 25 0 1 0 478947405 42295296 9388 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9388 603 41 0 10285 0
vsize: 41304
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9474 0 0 0 111977 39 0 0 25 0 1 0 478947405 42295296 9393 4294967295 134512640 134672761 3221224640 3221223744 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9393 603 41 0 10285 0
vsize: 41304
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9474 0 0 0 112977 39 0 0 25 0 1 0 478947405 42295296 9393 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10326 9393 603 41 0 10285 0
vsize: 41304
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9484 0 0 0 113977 39 0 0 25 0 1 0 478947405 42491904 9403 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10374 9403 603 41 0 10333 0
vsize: 41496
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9486 0 0 0 114977 39 0 0 25 0 1 0 478947405 42491904 9405 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10374 9405 603 41 0 10333 0
vsize: 41496
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9486 0 0 0 115977 39 0 0 25 0 1 0 478947405 42491904 9405 4294967295 134512640 134672761 3221224640 3221223744 134555133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10374 9405 603 41 0 10333 0
vsize: 41496
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9524 0 0 0 116977 39 0 0 25 0 1 0 478947405 42622976 9443 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10406 9443 603 41 0 10365 0
vsize: 41624
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 9840 0 0 0 117977 40 0 0 25 0 1 0 478947405 43827200 9759 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10700 9759 603 41 0 10659 0
vsize: 42800
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 10061 0 0 0 118977 40 0 0 25 0 1 0 478947405 44752896 9980 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10926 9980 603 41 0 10885 0
vsize: 43704
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 23254
Raw data (stat): 23189 (minisat+) R 23188 20024 20023 0 -1 0 10257 0 0 0 119976 41 0 0 25 0 1 0 478947405 45547520 10176 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11120 10176 603 41 0 11079 0
vsize: 44480
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 1/55 23254
Raw data (stat): 23189 (minisat+) Z 23188 20024 20023 0 -1 12 10260 0 0 0 119977 42 0 0 25 0 1 0 478947405 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.07
CPU time (s): 1200.2
CPU user time (s): 1199.77
CPU system time (s): 0.429934
CPU usage (%): 100.011
Max. virtual memory (Kb): 44480
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####