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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        851940 kB
Buffers:         40452 kB
Cached:         118260 kB
SwapCached:          0 kB
Active:         107000 kB
Inactive:        54856 kB
HighTotal:      131008 kB
HighFree:        19992 kB
LowTotal:       903652 kB
LowFree:        831948 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15160 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:37:22 (client local time) WITH STATUS 10 IN 1200.27 SECONDS
stats: 3931 7 1200.27 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 3575 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    3565     8250 |    1069       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1000          
c |         0 |    3565     8250 |    1426       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.104984 s)
c ==============================================================================
c [1mFound solution: 315[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:47988     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   60581   141333 |   18174       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/38063          
c   -- var.elim.:  2000/38063          
c   -- var.elim.:  3000/38063          
c   -- var.elim.:  4000/38063          
c   -- var.elim.:  5000/38063          
c   -- var.elim.:  6000/38063          
c   -- var.elim.:  7000/38063          
c   -- var.elim.:  8000/38063          
c   -- var.elim.:  9000/38063          
c   -- var.elim.:  10000/38063          
c   -- var.elim.:  11000/38063          
c   -- var.elim.:  12000/38063          
c   -- var.elim.:  13000/38063          
c   -- var.elim.:  14000/38063          
c   -- var.elim.:  15000/38063          
c   -- var.elim.:  16000/38063          
c   -- var.elim.:  17000/38063          
c   -- var.elim.:  18000/38063          
c   -- var.elim.:  19000/38063          
c   -- var.elim.:  20000/38063          
c   -- var.elim.:  21000/38063          
c   -- var.elim.:  22000/38063          
c   -- var.elim.:  23000/38063          
c   -- var.elim.:  24000/38063          
c   -- var.elim.:  25000/38063          
c   -- var.elim.:  26000/38063          
c   -- var.elim.:  27000/38063          
c   -- var.elim.:  28000/38063          
c   -- var.elim.:  29000/38063          
c   -- var.elim.:  30000/38063          
c   -- var.elim.:  31000/38063          
c   -- var.elim.:  32000/38063          
c   -- var.elim.:  33000/38063          
c   -- var.elim.:  34000/38063          
c   -- var.elim.:  35000/38063          
c   -- var.elim.:  36000/38063          
c   -- var.elim.:  37000/38063          
c   -- var.elim.:  38000/38063          
c   -- var.elim.:  38063/38063          
c   -- var.elim.:  1000/18653          
c   -- var.elim.:  2000/18653          
c   -- var.elim.:  3000/18653          
c   -- var.elim.:  4000/18653          
c   -- var.elim.:  5000/18653          
c   -- var.elim.:  6000/18653          
c   -- var.elim.:  7000/18653          
c   -- var.elim.:  8000/18653          
c   -- var.elim.:  9000/18653          
c   -- var.elim.:  10000/18653          
c   -- var.elim.:  11000/18653          
c   -- var.elim.:  12000/18653          
c   -- var.elim.:  13000/18653          
c   -- var.elim.:  14000/18653          
c   -- var.elim.:  15000/18653          
c   -- var.elim.:  16000/18653          
c   -- var.elim.:  17000/18653          
c   -- var.elim.:  18000/18653          
c   -- var.elim.:  18653/18653          
c   -- var.elim.:  1000/11293          
c   -- var.elim.:  2000/11293          
c   -- var.elim.:  3000/11293          
c   -- var.elim.:  4000/11293          
c   -- var.elim.:  5000/11293          
c   -- var.elim.:  6000/11293          
c   -- var.elim.:  7000/11293          
c   -- var.elim.:  8000/11293          
c   -- var.elim.:  9000/11293          
c   -- var.elim.:  10000/11293          
c   -- var.elim.:  11000/11293          
c   -- var.elim.:  11293/11293          
c   -- var.elim.:  1000/7877          
c   -- var.elim.:  2000/7877          
c   -- var.elim.:  3000/7877          
c   -- var.elim.:  4000/7877          
c   -- var.elim.:  5000/7877          
c   -- var.elim.:  6000/7877          
c   -- var.elim.:  7000/7877          
c   -- var.elim.:  7877/7877          
c   -- var.elim.:  1000/6855          
c   -- var.elim.:  2000/6855          
c   -- var.elim.:  3000/6855          
c   -- var.elim.:  4000/6855          
c   -- var.elim.:  5000/6855          
c   -- var.elim.:  6000/6855          
c   -- var.elim.:  6855/6855          
c   -- var.elim.:  1000/4999          
c   -- var.elim.:  2000/4999          
c   -- var.elim.:  3000/4999          
c   -- var.elim.:  4000/4999          
c   -- var.elim.:  4999/4999          
c   -- var.elim.:  1000/3466          
c   -- var.elim.:  2000/3466          
c   -- var.elim.:  3000/3466          
c   -- var.elim.:  3466/3466          
c   -- var.elim.:  137/137          
c   -- var.elim.:  370/370          
c   -- var.elim.:  58/58          
c   -- subsuming                       
c   -- var.elim.:  1000/6318          
c   -- var.elim.:  2000/6318          
c   -- var.elim.:  3000/6318          
c   -- var.elim.:  4000/6318          
c   -- var.elim.:  5000/6318          
c   -- var.elim.:  6000/6318          
c   -- var.elim.:  6318/6318          
c |         0 |   20531   126180 |      --       0       --      -- |     --   | -40050/-15152
c |         0 |   20531   126180 |    8212       0        0     nan |  0.000 % |
c |       100 |   20258   120547 |    8913      87     4048    46.5 |  1.178 % |
c |       251 |   20133   119579 |    9744     233    11182    48.0 |  1.790 % |
c |       476 |   19842   117375 |   10563     446    23037    51.7 |  3.251 % |
c |       813 |   19817   117153 |   11605     782    55049    70.4 |  3.387 % |
c |      1321 |   18686   108563 |   12037    1243    98886    79.6 |  9.198 % |
c |      2080 |   18431   106625 |   13060    1985   160911    81.1 | 10.512 % |
c |      3219 |   17749   101033 |   13835    3077   284207    92.4 | 14.069 % |
c |      4929 |   17463    98785 |   14973    4725   442538    93.7 | 15.632 % |
c |      7497 |   17463    98785 |   16470    7293   761669   104.4 | 15.632 % |
c |     11341 |   17457    98731 |   18111   11127  1340187   120.4 | 15.666 % |
c |     17107 |   17435    98573 |   19897   16892  2196947   130.1 | 15.768 % |
c |     25756 |   17352    98004 |   21783   12857  2634217   204.9 | 16.210 % |
c |     38731 |   17297    97532 |   23885   25816  7283986   282.2 | 16.516 % |
c |     58193 |   17297    97532 |   26274   14824  4673169   315.2 | 16.516 % |
c |     87390 |   17297    97532 |   28901   26849  4373652   162.9 | 16.516 % |
c |    131181 |   17297    97532 |   31791   31834 14948237   469.6 | 16.516 % |
c |    196867 |   17277    97384 |   34930   31905 18218361   571.0 | 16.618 % |
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 x752 -x753 x754 -x755 x756 -x757 x758 -x759 x760 -x761 x762 -x763 x764 x765 -x766 -x767 -x768 -x769 -x770 -x771 -x772 -x773 -x774 -x775 -x776 -x777 -x778 -x779 -x780 x781 -x782 -x783 -x784 -x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 -x794 -x795 -x796 -x797 -x798 -x799 -x800 x801 -x802 -x803 x804 -x805 -x806 -x807 -x808 -x809 -x810 -x811 -x812 -x813 -x814 -x815 -x816 -x817 -x818 -x819 -x820 x821 -x822 -x823 -x824 -x825 -x826 -x827 -x828 -x829 -x830 -x831 -x832 -x833 -x834 -x835 -x836 -x837 -x838 -x839 -x840 x841 -x842 -x843 x844 -x845 -x846 -x847 -x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 -x860 -x861 x862 -x863 x864 x865 -x866 -x867 -x868 -x869 -x870 -x871 -x872 -x873 -x874 -x875 -x876 -x877 -x878 -x879 -x880 x881 -x882 -x883 x884 -x885 -x886 -x887 -x888 -x889 -x890 -x891 -x892 -x893 -x894 -x895 -x896 -x897 -x898 -x899 -x900 -x901 x902 x903 -x904 -x905 x906 -x907 x908 -x909 x910 -x911 x912 -x913 x914 -x915 x916 -x917 x918 -x919 x920 -x921 x922 -x923 x924 x925 -x926 -x927 -x928 -x929 -x930 -x931 -x932 -x933 -x934 -x935 -x936 -x937 -x938 -x939 -x940 x941 -x942 -x943 x944 -x945 -x946 -x947 -x948 -x949 -x950 -x951 -x952 -x953 -x954 -x955 -x956 -x957 -x958 -x959 -x960 x961 -x962 -x963 -x964 -x965 -x966 -x967 -x968 -x969 -x970 -x971 -x972 -x973 -x974 -x975 -x976 -x977 -x9#### 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.85 0.94 0.90 2/56 18607
Raw data (stat): 18607 (runsolver) D 18606 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 365129535 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 5772 0 0 0 979 19 0 0 25 0 1 0 365129535 26890240 5472 4294967295 134512640 134672761 3221224576 3221223024 134643567 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6565 5472 603 41 0 6524 0
vsize: 26260
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 5827 0 0 0 1969 28 0 0 25 0 1 0 365129535 27152384 5527 4294967295 134512640 134672761 3221224576 3221223024 134643636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6629 5527 603 41 0 6588 0
vsize: 26516
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.94 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 5828 0 0 0 2969 29 0 0 25 0 1 0 365129535 26890240 5490 4294967295 134512640 134672761 3221224576 3221223068 134642915 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6565 5490 603 41 0 6524 0
vsize: 26260
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.94 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 5909 0 0 0 3969 29 0 0 25 0 1 0 365129535 26890240 5511 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6565 5511 603 41 0 6524 0
vsize: 26260
[startup+50.0036 s]
Raw data (loadavg): 0.93 0.94 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 6191 0 0 0 4969 29 0 0 25 0 1 0 365129535 28090368 5793 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6858 5793 603 41 0 6817 0
vsize: 27432
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.90 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 7220 0 0 0 5966 32 0 0 25 0 1 0 365129535 32284672 6822 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7882 6822 603 41 0 7841 0
vsize: 31528
[startup+70.0038 s]
Raw data (loadavg): 0.95 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 7904 0 0 0 6964 35 0 0 25 0 1 0 365129535 35143680 7506 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8580 7506 603 41 0 8539 0
vsize: 34320
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 9157 0 0 0 7961 38 0 0 25 0 1 0 365129535 40263680 8759 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9830 8759 603 41 0 9789 0
vsize: 39320
[startup+90.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 9460 0 0 0 8960 39 0 0 25 0 1 0 365129535 41410560 9062 4294967295 134512640 134672761 3221224576 3221223760 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10110 9062 603 41 0 10069 0
vsize: 40440
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 10279 0 0 0 9959 40 0 0 25 0 1 0 365129535 44802048 9881 4294967295 134512640 134672761 3221224576 3221223600 134612944 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10938 9881 603 41 0 10897 0
vsize: 43752
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 11988 0 0 0 10955 45 0 0 25 0 1 0 365129535 51847168 11590 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12658 11590 603 41 0 12617 0
vsize: 50632
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 12859 0 0 0 11953 47 0 0 25 0 1 0 365129535 55320576 12460 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13506 12460 603 41 0 13465 0
vsize: 54024
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 12859 0 0 0 12953 47 0 0 25 0 1 0 365129535 55320576 12460 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13506 12460 603 41 0 13465 0
vsize: 54024
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 13139 0 0 0 13953 48 0 0 25 0 1 0 365129535 56516608 12740 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13798 12740 603 41 0 13757 0
vsize: 55192
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14102 0 0 0 14951 50 0 0 25 0 1 0 365129535 60448768 13703 4294967295 134512640 134672761 3221224576 3221223616 134613756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14758 13703 603 41 0 14717 0
vsize: 59032
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14757 0 0 0 15948 52 0 0 25 0 1 0 365129535 63062016 14357 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15396 14357 603 41 0 15355 0
vsize: 61584
[startup+170.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14757 0 0 0 16949 52 0 0 25 0 1 0 365129535 63062016 14357 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15396 14357 603 41 0 15355 0
vsize: 61584
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14757 0 0 0 17949 52 0 0 25 0 1 0 365129535 63062016 14357 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15396 14357 603 41 0 15355 0
vsize: 61584
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14757 0 0 0 18949 52 0 0 25 0 1 0 365129535 63062016 14357 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15396 14357 603 41 0 15355 0
vsize: 61584
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14758 0 0 0 19949 52 0 0 25 0 1 0 365129535 63057920 14357 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14357 603 41 0 15354 0
vsize: 61580
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14758 0 0 0 20949 52 0 0 25 0 1 0 365129535 63057920 14357 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14357 603 41 0 15354 0
vsize: 61580
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14758 0 0 0 21950 52 0 0 25 0 1 0 365129535 63057920 14357 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14357 603 41 0 15354 0
vsize: 61580
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18607
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14758 0 0 0 22950 52 0 0 25 0 1 0 365129535 63057920 14357 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14357 603 41 0 15354 0
vsize: 61580
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 23950 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 24950 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 25950 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 26951 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 27951 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14760 0 0 0 28951 52 0 0 25 0 1 0 365129535 63057920 14359 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15395 14359 603 41 0 15354 0
vsize: 61580
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14841 0 0 0 29951 52 0 0 25 0 1 0 365129535 63369216 14437 4294967295 134512640 134672761 3221224576 3221223616 134612867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15471 14437 603 41 0 15430 0
vsize: 61884
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14841 0 0 0 30951 52 0 0 25 0 1 0 365129535 63369216 14437 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15471 14437 603 41 0 15430 0
vsize: 61884
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 14841 0 0 0 31952 52 0 0 25 0 1 0 365129535 63369216 14437 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15471 14437 603 41 0 15430 0
vsize: 61884
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 15718 0 0 0 32949 55 0 0 25 0 1 0 365129535 67010560 15314 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16360 15314 603 41 0 16319 0
vsize: 65440
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 16900 0 0 0 33946 58 0 0 25 0 1 0 365129535 71864320 16496 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17545 16496 603 41 0 17504 0
vsize: 70180
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 18062 0 0 0 34943 61 0 0 25 0 1 0 365129535 76668928 17658 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18718 17658 603 41 0 18677 0
vsize: 74872
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 19414 0 0 0 35940 64 0 0 25 0 1 0 365129535 82132992 19010 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20052 19010 603 41 0 20011 0
vsize: 80208
[startup+370.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 20486 0 0 0 36938 67 0 0 25 0 1 0 365129535 86601728 20082 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21143 20082 603 41 0 21102 0
vsize: 84572
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 21413 0 0 0 37936 69 0 0 25 0 1 0 365129535 90394624 21009 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22069 21009 603 41 0 22028 0
vsize: 88276
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 22446 0 0 0 38934 71 0 0 25 0 1 0 365129535 94605312 22042 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23097 22042 603 41 0 23056 0
vsize: 92388
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 39932 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 40932 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 41932 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 42932 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 43932 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 44933 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 45933 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 46933 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 23501 0 0 0 47933 73 0 0 25 0 1 0 365129535 98840576 23091 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24131 23091 603 41 0 24090 0
vsize: 96524
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24523 0 0 0 48930 76 0 0 25 0 1 0 365129535 103120896 24113 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25176 24113 603 41 0 25135 0
vsize: 100704
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 49930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+510.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 50930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 51930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18609
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 52930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+540.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 53930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+550.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 54930 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 55931 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24847 0 0 0 56931 77 0 0 25 0 1 0 365129535 104329216 24431 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24431 603 41 0 25430 0
vsize: 101884
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24849 0 0 0 57931 77 0 0 25 0 1 0 365129535 104329216 24433 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24433 603 41 0 25430 0
vsize: 101884
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24849 0 0 0 58931 77 0 0 25 0 1 0 365129535 104329216 24433 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 24433 603 41 0 25430 0
vsize: 101884
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 59931 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 60931 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223584 134522545 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 61931 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+630.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 62932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 63932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 64932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 65932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 66932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223712 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+680.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 24965 0 0 0 67932 77 0 0 25 0 1 0 365129535 104656896 24513 4294967295 134512640 134672761 3221224576 3221223448 1075353087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25551 24513 603 41 0 25510 0
vsize: 102204
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 25938 0 0 0 68930 80 0 0 25 0 1 0 365129535 108691456 25486 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26536 25486 603 41 0 26495 0
vsize: 106144
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 27136 0 0 0 69927 83 0 0 25 0 1 0 365129535 113623040 26684 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27740 26684 603 41 0 27699 0
vsize: 110960
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 27899 0 0 0 70926 85 0 0 25 0 1 0 365129535 116748288 27447 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28503 27447 603 41 0 28462 0
vsize: 114012
[startup+720.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 28834 0 0 0 71923 88 0 0 25 0 1 0 365129535 120520704 28382 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29424 28382 603 41 0 29383 0
vsize: 117696
[startup+730.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 29670 0 0 0 72922 89 0 0 25 0 1 0 365129535 124026880 29218 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30280 29218 603 41 0 30239 0
vsize: 121120
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 73919 92 0 0 25 0 1 0 365129535 128999424 30431 4294967295 134512640 134672761 3221224576 3221223632 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31494 30431 603 41 0 31453 0
vsize: 125976
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 74919 92 0 0 25 0 1 0 365129535 128868352 30422 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30422 603 41 0 31421 0
vsize: 125848
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 75919 92 0 0 25 0 1 0 365129535 128868352 30422 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30422 603 41 0 31421 0
vsize: 125848
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 76920 92 0 0 25 0 1 0 365129535 128868352 30422 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30422 603 41 0 31421 0
vsize: 125848
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 77920 92 0 0 25 0 1 0 365129535 128868352 30422 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30422 603 41 0 31421 0
vsize: 125848
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30883 0 0 0 78920 92 0 0 25 0 1 0 365129535 128868352 30422 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30422 603 41 0 31421 0
vsize: 125848
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 79920 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 80920 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 81920 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18611
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 82921 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 83921 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+850.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30884 0 0 0 84921 92 0 0 25 0 1 0 365129535 128868352 30423 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31462 30423 603 41 0 31421 0
vsize: 125848
[startup+860.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 85921 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223616 134612827 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 86921 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+880.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 87921 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+890.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 88921 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+900.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 89922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+910.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 90922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 91922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 92922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 93922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+950.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 94922 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+960.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 95923 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 96923 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 30922 0 0 0 97923 92 0 0 25 0 1 0 365129535 128843776 30417 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31456 30417 603 41 0 31415 0
vsize: 125824
[startup+990.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31000 0 0 0 98923 92 0 0 25 0 1 0 365129535 129224704 30495 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31549 30495 603 41 0 31508 0
vsize: 126196
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 99923 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 100923 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 101923 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 102923 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 103924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 104924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 105924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 106924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 107924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 108924 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 109925 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223616 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 110925 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 31146 0 0 0 111925 93 0 0 25 0 1 0 365129535 129601536 30602 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31641 30602 603 41 0 31600 0
vsize: 126564
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18613
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 32058 0 0 0 112922 95 0 0 25 0 1 0 365129535 133406720 31514 4294967295 134512640 134672761 3221224576 3221223408 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32570 31514 603 41 0 32529 0
vsize: 130280
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33240 0 0 0 113920 98 0 0 25 0 1 0 365129535 138219520 32696 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33745 32696 603 41 0 33704 0
vsize: 134980
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 114917 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 115917 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 116918 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 117918 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 118918 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 18615
Raw data (stat): 18607 (minisat+) R 18606 12452 12451 0 -1 0 33902 0 0 0 119918 101 0 0 25 0 1 0 365129535 140853248 33349 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34388 33349 603 41 0 34347 0
vsize: 137552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 18615
Raw data (stat): 18607 (minisat+) Z 18606 12452 12451 0 -1 12 33903 0 0 0 119918 108 0 0 25 0 1 0 365129535 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.27
CPU user time (s): 1199.19
CPU system time (s): 1.08283
CPU usage (%): 100.015
Max. virtual memory (Kb): 137552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####