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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namesubmitted/manquinho/primes-dimacs-cnf/normalized-ii8e2.opb
MD5SUM66ef5c48f4a7492e24281157b7778ffb
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 494
Optimality of the best value was proved NO
Number of terms in the objective function 1740
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 1740
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1740
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.12
Number of variables1740
Total number of constraints6991
Number of constraints which are clauses6991
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint10

Trace number 1531

Launcher Data

LAUNCH ON wulflinc26 THE 2005-09-18 15:29:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2510 boxname=wulflinc26 idbench=166 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  66ef5c48f4a7492e24281157b7778ffb  /oldhome/oroussel/tmp/wulflinc26/normalized-ii8e2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-ii8e2.opb
IDLAUNCH: 2510
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        922660 kB
Buffers:         35252 kB
Cached:          49764 kB
SwapCached:        868 kB
Active:          64752 kB
Inactive:        22880 kB
HighTotal:      131008 kB
HighFree:        78540 kB
LowTotal:       903652 kB
LowFree:        844120 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18860 kB
Committed_AS:    64132 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 15:49:15 (client local time) WITH STATUS 10 IN 1208.23 SECONDS
stats: 2510 7 1208.23 10

Solver Data

c Parsing PB file...
c Converting 6991 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 |    6991    16290 |    2330       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 590
c ---[   0]---> Sorter-cost:98402     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         4 |  128567   300131 |   42855       4       22     5.5 |  0.000 % |
c |       106 |  128430   299852 |   47140     102     3326    32.6 |  0.102 % |
c |       257 |  128430   299852 |   51854     253     7574    29.9 |  0.102 % |
c |       482 |  128430   299852 |   57040     478    12756    26.7 |  0.102 % |
c |       819 |  128430   299852 |   62744     815    19346    23.7 |  0.102 % |
c |      1326 |  127377   297611 |   69018    1223    87028    71.2 |  0.826 % |
c |      2085 |  127264   297372 |   75920    1980   106712    53.9 |  0.903 % |
c |      3225 |  127264   297372 |   83512    3120   139734    44.8 |  0.903 % |
c |      4933 |  127208   297252 |   91863    4827   190149    39.4 |  0.942 % |
c |      7495 |  126172   294982 |  101049    7371   620898    84.2 |  1.694 % |
c |     11339 |  126168   294974 |  111154   11213   773205    69.0 |  1.696 % |
c ==============================================================================
c Found solution: 574
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15699 |  126007   294731 |   42002   15567  2039083   131.0 |  1.696 % |
c |     15799 |  125560   293728 |   46202   15658  2041962   130.4 |  2.288 % |
c |     15954 |  125468   293528 |   50822   15793  2051349   129.9 |  2.354 % |
c |     16182 |  125045   292603 |   55904   16012  2055877   128.4 |  2.660 % |
c |     16523 |  125045   292603 |   61495   16353  2063549   126.2 |  2.660 % |
c |     17031 |  125041   292595 |   67644   16860  2075782   123.1 |  2.662 % |
c |     17790 |  125041   292595 |   74409   17619  2121233   120.4 |  2.662 % |
c |     18929 |  124707   291849 |   81850   18753  2161700   115.3 |  2.913 % |
c |     20638 |  124446   291276 |   90035   20456  2323907   113.6 |  3.102 % |
c ==============================================================================
c Found solution: 555
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21743 |  124549   291618 |   41516   21386  2359361   110.3 |  3.102 % |
c |     21843 |  124523   291562 |   45667   21485  2368288   110.2 |  3.194 % |
c |     21993 |  124523   291562 |   50234   21635  2372240   109.6 |  3.194 % |
c |     22219 |  124523   291562 |   55257   21861  2378958   108.8 |  3.194 % |
c |     22556 |  124263   290984 |   60783   22191  2414231   108.8 |  3.388 % |
c |     23063 |  124080   290577 |   66861   22674  2426492   107.0 |  3.524 % |
c |     23822 |  124080   290577 |   73548   23433  2454764   104.8 |  3.524 % |
c |     24961 |  123797   289950 |   80902   24567  2535712   103.2 |  3.732 % |
c ==============================================================================
c Found solution: 494
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25686 |  124281   291166 |   41427   25208  2510359    99.6 |  3.732 % |
c |     25788 |  124281   291166 |   45569   25310  2517812    99.5 |  3.736 % |
c |     25941 |  124281   291166 |   50126   25463  2521177    99.0 |  3.736 % |
c |     26166 |  124281   291166 |   55139   25688  2544728    99.1 |  3.736 % |
c |     26504 |  124281   291166 |   60653   26026  2552818    98.1 |  3.736 % |
c |     27010 |  124281   291166 |   66718   26532  2566479    96.7 |  3.736 % |
c |     27769 |  124281   291166 |   73390   27291  2649683    97.1 |  3.736 % |
c |     28909 |  124268   291139 |   80729   28426  2831024    99.6 |  3.745 % |
c |     30620 |  123560   289545 |   88802   30124  2971797    98.7 |  4.281 % |
c |     33183 |  123560   289545 |   97682   32687  3060042    93.6 |  4.281 % |
c |     37027 |  122823   287902 |  107450   36485  3318331    91.0 |  4.829 % |
c |     42795 |  122823   287902 |  118196   42253  3563411    84.3 |  4.829 % |
c |     51444 |  122349   286858 |  130015   50853  4043393    79.5 |  5.174 % |
c |     64418 |  122229   286580 |  143017   63803  4620873    72.4 |  5.269 % |
c |     83879 |  121410   284759 |  157318   83153  7456425    89.7 |  5.875 % |
c |    113072 |  121372   284671 |  173050  112319 10057431    89.5 |  5.906 % |
c |    156862 |  121119   284108 |  190355  156017 12155915    77.9 |  6.093 % |
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 x978 -x979 x980 -x981 -x982 -x983 -x984 -x985 -x986 -x987 x988 x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 -x1000 -x1001 x1002 -x1003 x1004 -x1005 x1006 x1007 -x1008 -x1009 -x1010 -x1011 x1012 -x1013 x1014 -x1015 x1016 -x1017 x1018 -x1019 x1020 -x1021 x1022 -x1023 x1024 -x1025 x1026 x1027 -x1028 -x1029 x1030 -x1031 x1032 -x1033 x1034 -x1035 x1036 -x1037 x1038 -x1039 x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 x1048 -x1049 x1050 -x1051 -x1052 -x1053 -x1054 x1055 -x1056 -x1057 -x1058 -x1059 -x1060 -x1061 x1062 -x1063 x1064 -x1065 x1066 -x1067 x1068 x1069 -x1070 -x1071 x1072 -x1073 x1074 -x1075 x1076 -x1077 x1078 -x1079 x1080 -x1081 -x1082 -x1083 -x1084 x1085 -x1086 -x1087 x1088 -x1089 -x1090 -x1091 -x1092 -x1093 -x1094 -x1095 -x1096 -x1097 -x1098 -x1099 -x1100 -x1101 x1102 -x1103 x1104 -x1105 x1106 x1107 -x1108 -x1109 -x1110 -x1111 x1112 -x1113 x1114 -x1115 x1116 -x1117 x1118 -x1119 x1120 x1121 -x1122 -x1123 -x1124 -x1125 -x1126 -x1127 -x1128 -x1129 -x1130 -x1131 -x1132 -x1133 -x1134 -x1135 -x1136 -x1137 -x1138 -x1139 -x1140 -x1141 -x1142 x1143 -x1144 -x1145 -x1146 -x1147 x1148 -x1149 x1150 -x1151 -x1152 -x1153 -x1154 -x1155 -x1156 -x1157 -x1158 -x1159 -x1160 -x1161 -x1162 -x1163 -x1164 -x1165 -x1166 -x1167 x1168 -x1169 x1170 -x1171 -x1172 x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 -x1180 -x1181 -x1182 -x1183 -x1184 -x1185 -x1186 -x1187 -x1188 -x1189 x1190 -x1191 -x1192 -x1193 -x1194 -x1195 -x1196 -x1197 -x1198 x1199 -x1200 -x1201 -x1202 -x1203 -x1204 -x1205 -x1206 -x1207 x1208 -x1209 x1210 -x1211 -x1212 -x1213 -x1214 x1215 -x1216 -x1217 -x1218 -x1219 -x1220 -x1221 -x1222 -x1223 -x1224 -x1225 -x1226 -x1227 x1228 -x1229 -x1230 -x1231 -x1232 -x1233 -x1234 x1235 -x1236 -x1237 -x1238 -x1239 -x1240 -x1241 -x1242 -x1243 -x1244 -x1245 -x1246 -x1247 x1248 -x1249 x1250 x1251 -x1252 -x1253 -x1254 -x1255 -x1256 -x1257 -x1258 -x1259 -x1260 -x1261 -x1262 x1263 -x1264 -x1265 -x1266 -x1267 x1268 -x1269 -x1270 -x1271 -x1272 -x1273 -x1274 -x1275 -x1276 -x1277 -x1278 -x1279 -x1280 -x1281 x1282 -x1283 x1284 -x1285 x1286 -x1287 x1288 x1289 -x1290 -x1291 x1292 -x1293 x1294 -x1295 x1296 -x1297 x1298 -x1299 x1300 -x1301 -x1302 -x1303 -x1304 -x1305 -x1306 -x1307 -x1308 -x1309 x1310 -x1311 -x1312 -x1313 -x1314 x1315 -x1316 -x1317 -x1318 -x1319 -x1320 -x1321 x1322 -x1323 x1324 -x1325 x1326 x1327 -x1328 -x1329 x1330 -x1331 x1332 -x1333 x1334 -x1335 x1336 -x1337 x1338 -x1339 x1340 -x1341 x1342 -x1343 x1344 -x1345 x1346 -x1347 x1348 x1349 -x1350 -x1351 x1352 -x1353 x1354 -x1355 x1356 -x1357 x1358 -x1359 x1360 -x1361 -x1362 -x1363 -x1364 -x1365 -x1366 -x1367 -x1368 -x1369 x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 -x1377 -x1378 x1379 -x1380 x1381 -x1382 -x1383

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/22144/stat): 22144 (minisat+_script) R 22143 22144 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842350917 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/22144/statm): 174 3 169 147 0 27 0
[pid=22144] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=22145
New process pid=22146
New process pid=22147
execve syscall for /bin/sed executable
One traced child (pid=22146) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=22147) exited with status: 0
One traced child (pid=22145) exited with status: 0
New process pid=22148
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-ii8e2.opb

[startup+10.004 s]
Raw data (loadavg): 0.93 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 6629 0 0 0 945 23 0 0 25 0 1 0 1842350922 29675520 6313 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 7245 6313 145 145 0 7100 0
[pid=22148] vsize: 28980
Current children cumulated CPU time (s) 9.68
Current children cumulated vsize (Kb) 31104

[startup+20.0046 s]
Raw data (loadavg): 0.94 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 6729 0 0 0 1942 25 0 0 25 0 1 0 1842350922 30085120 6413 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 7345 6413 145 145 0 7200 0
[pid=22148] vsize: 29380
Current children cumulated CPU time (s) 19.67
Current children cumulated vsize (Kb) 31504

[startup+30.0063 s]
Raw data (loadavg): 0.95 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 6857 0 0 0 2939 27 0 0 25 0 1 0 1842350922 30597120 6541 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 7470 6541 145 145 0 7325 0
[pid=22148] vsize: 29880
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 32004

[startup+40.007 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 7225 0 0 0 3934 28 0 0 25 0 1 0 1842350922 32100352 6909 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 7837 6909 145 145 0 7692 0
[pid=22148] vsize: 31348
Current children cumulated CPU time (s) 39.62
Current children cumulated vsize (Kb) 33472

[startup+50.0087 s]
Raw data (loadavg): 0.96 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 7349 0 0 0 4931 30 0 0 25 0 1 0 1842350922 32628736 7033 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 7966 7033 145 145 0 7821 0
[pid=22148] vsize: 31864
Current children cumulated CPU time (s) 49.61
Current children cumulated vsize (Kb) 33988

[startup+60.0094 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 7613 0 0 0 5927 31 0 0 25 0 1 0 1842350922 33726464 7297 4294967295 134512640 135094434 3221224448 3221223040 134556949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 8234 7297 145 145 0 8089 0
[pid=22148] vsize: 32936
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 35060

[startup+70.01 s]
Raw data (loadavg): 0.97 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 7950 0 0 0 6923 33 0 0 25 0 1 0 1842350922 35098624 7634 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 8569 7634 145 145 0 8424 0
[pid=22148] vsize: 34276
Current children cumulated CPU time (s) 69.56
Current children cumulated vsize (Kb) 36400

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 8356 0 0 0 7918 35 0 0 25 0 1 0 1842350922 36749312 8040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 8972 8040 145 145 0 8827 0
[pid=22148] vsize: 35888
Current children cumulated CPU time (s) 79.53
Current children cumulated vsize (Kb) 38012

[startup+90.0124 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 8642 0 0 0 8915 36 0 0 25 0 1 0 1842350922 37904384 8326 4294967295 134512640 135094434 3221224448 3221223104 134558366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 9254 8326 145 145 0 9109 0
[pid=22148] vsize: 37016
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 39140

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 8933 0 0 0 9913 38 0 0 25 0 1 0 1842350922 39473152 8617 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 9637 8617 145 145 0 9492 0
[pid=22148] vsize: 38548
Current children cumulated CPU time (s) 99.51
Current children cumulated vsize (Kb) 40672

[startup+110.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 8988 0 0 0 10911 39 0 0 25 0 1 0 1842350922 39739392 8672 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 9702 8672 145 145 0 9557 0
[pid=22148] vsize: 38808
Current children cumulated CPU time (s) 109.5
Current children cumulated vsize (Kb) 40932

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9096 0 0 0 11909 39 0 0 25 0 1 0 1842350922 40181760 8780 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 9810 8780 145 145 0 9665 0
[pid=22148] vsize: 39240
Current children cumulated CPU time (s) 119.48
Current children cumulated vsize (Kb) 41364

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9326 0 0 0 12906 41 0 0 25 0 1 0 1842350922 40976384 8975 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10004 8975 145 145 0 9859 0
[pid=22148] vsize: 40016
Current children cumulated CPU time (s) 129.47
Current children cumulated vsize (Kb) 42140

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9401 0 0 0 13905 41 0 0 25 0 1 0 1842350922 41275392 9050 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10077 9050 145 145 0 9932 0
[pid=22148] vsize: 40308
Current children cumulated CPU time (s) 139.46
Current children cumulated vsize (Kb) 42432

[startup+150.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9586 0 0 0 14903 42 0 0 25 0 1 0 1842350922 42020864 9235 4294967295 134512640 135094434 3221224448 3220988400 134596854 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10259 9235 145 145 0 10114 0
[pid=22148] vsize: 41036
Current children cumulated CPU time (s) 149.45
Current children cumulated vsize (Kb) 43160

[startup+160.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9704 0 0 0 15902 43 0 0 25 0 1 0 1842350922 42344448 9320 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10338 9320 145 145 0 10193 0
[pid=22148] vsize: 41352
Current children cumulated CPU time (s) 159.45
Current children cumulated vsize (Kb) 43476

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 9920 0 0 0 16899 44 0 0 25 0 1 0 1842350922 43225088 9536 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10553 9536 145 145 0 10408 0
[pid=22148] vsize: 42212
Current children cumulated CPU time (s) 169.43
Current children cumulated vsize (Kb) 44336

[startup+180.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10054 0 0 0 17897 45 0 0 25 0 1 0 1842350922 43765760 9670 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10685 9670 145 145 0 10540 0
[pid=22148] vsize: 42740
Current children cumulated CPU time (s) 179.42
Current children cumulated vsize (Kb) 44864

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10190 0 0 0 18895 46 0 0 25 0 1 0 1842350922 44445696 9806 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 10851 9806 145 145 0 10706 0
[pid=22148] vsize: 43404
Current children cumulated CPU time (s) 189.41
Current children cumulated vsize (Kb) 45528

[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10365 0 0 0 19892 47 0 0 25 0 1 0 1842350922 45154304 9981 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11024 9981 145 145 0 10879 0
[pid=22148] vsize: 44096
Current children cumulated CPU time (s) 199.39
Current children cumulated vsize (Kb) 46220

[startup+210.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10451 0 0 0 20891 48 0 0 25 0 1 0 1842350922 45502464 10067 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11109 10067 145 145 0 10964 0
[pid=22148] vsize: 44436
Current children cumulated CPU time (s) 209.39
Current children cumulated vsize (Kb) 46560

[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10596 0 0 0 21889 49 0 0 25 0 1 0 1842350922 46084096 10212 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11251 10212 145 145 0 11106 0
[pid=22148] vsize: 45004
Current children cumulated CPU time (s) 219.38
Current children cumulated vsize (Kb) 47128

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10740 0 0 0 22886 50 0 0 25 0 1 0 1842350922 46661632 10356 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11392 10356 145 145 0 11247 0
[pid=22148] vsize: 45568
Current children cumulated CPU time (s) 229.36
Current children cumulated vsize (Kb) 47692

[startup+240.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10857 0 0 0 23883 51 0 0 25 0 1 0 1842350922 47132672 10473 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11507 10473 145 145 0 11362 0
[pid=22148] vsize: 46028
Current children cumulated CPU time (s) 239.34
Current children cumulated vsize (Kb) 48152

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 10961 0 0 0 24882 52 0 0 25 0 1 0 1842350922 47546368 10577 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11608 10577 145 145 0 11463 0
[pid=22148] vsize: 46432
Current children cumulated CPU time (s) 249.34
Current children cumulated vsize (Kb) 48556

[startup+260.027 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11183 0 0 0 25878 53 0 0 25 0 1 0 1842350922 48451584 10799 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11829 10799 145 145 0 11684 0
[pid=22148] vsize: 47316
Current children cumulated CPU time (s) 259.31
Current children cumulated vsize (Kb) 49440

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11330 0 0 0 26876 54 0 0 25 0 1 0 1842350922 49049600 10946 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 11975 10946 145 145 0 11830 0
[pid=22148] vsize: 47900
Current children cumulated CPU time (s) 269.3
Current children cumulated vsize (Kb) 50024

[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11451 0 0 0 27874 55 0 0 25 0 1 0 1842350922 49537024 11067 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 12094 11067 145 145 0 11949 0
[pid=22148] vsize: 48376
Current children cumulated CPU time (s) 279.29
Current children cumulated vsize (Kb) 50500

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11583 0 0 0 28872 55 0 0 25 0 1 0 1842350922 50061312 11199 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 12222 11199 145 145 0 12077 0
[pid=22148] vsize: 48888
Current children cumulated CPU time (s) 289.27
Current children cumulated vsize (Kb) 51012

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11713 0 0 0 29870 57 0 0 25 0 1 0 1842350922 50581504 11329 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 12349 11329 145 145 0 12204 0
[pid=22148] vsize: 49396
Current children cumulated CPU time (s) 299.27
Current children cumulated vsize (Kb) 51520

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11858 0 0 0 30867 58 0 0 25 0 1 0 1842350922 51159040 11474 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 12490 11474 145 145 0 12345 0
[pid=22148] vsize: 49960
Current children cumulated CPU time (s) 309.25
Current children cumulated vsize (Kb) 52084

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 11961 0 0 0 31866 59 0 0 25 0 1 0 1842350922 51576832 11577 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 12592 11577 145 145 0 12447 0
[pid=22148] vsize: 50368
Current children cumulated CPU time (s) 319.25
Current children cumulated vsize (Kb) 52492

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12052 0 0 0 32864 60 0 0 25 0 1 0 1842350922 51945472 11668 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 12682 11668 145 145 0 12537 0
[pid=22148] vsize: 50728
Current children cumulated CPU time (s) 329.24
Current children cumulated vsize (Kb) 52852

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12130 0 0 0 33862 61 0 0 25 0 1 0 1842350922 52260864 11746 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 12759 11746 145 145 0 12614 0
[pid=22148] vsize: 51036
Current children cumulated CPU time (s) 339.23
Current children cumulated vsize (Kb) 53160

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12346 0 0 0 34857 64 0 0 25 0 1 0 1842350922 53403648 11962 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 13038 11962 145 145 0 12893 0
[pid=22148] vsize: 52152
Current children cumulated CPU time (s) 349.21
Current children cumulated vsize (Kb) 54276

[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12565 0 0 0 35854 65 0 0 25 0 1 0 1842350922 54292480 12181 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 13255 12181 145 145 0 13110 0
[pid=22148] vsize: 53020
Current children cumulated CPU time (s) 359.19
Current children cumulated vsize (Kb) 55144

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12737 0 0 0 36851 66 0 0 25 0 1 0 1842350922 54992896 12353 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 13426 12353 145 145 0 13281 0
[pid=22148] vsize: 53704
Current children cumulated CPU time (s) 369.17
Current children cumulated vsize (Kb) 55828

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 12947 0 0 0 37847 68 0 0 25 0 1 0 1842350922 55848960 12563 4294967295 134512640 135094434 3221224448 3221223040 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 13635 12563 145 145 0 13490 0
[pid=22148] vsize: 54540
Current children cumulated CPU time (s) 379.15
Current children cumulated vsize (Kb) 56664

[startup+390.038 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 13133 0 0 0 38845 69 0 0 25 0 1 0 1842350922 56606720 12749 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 13820 12749 145 145 0 13675 0
[pid=22148] vsize: 55280
Current children cumulated CPU time (s) 389.14
Current children cumulated vsize (Kb) 57404

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 13364 0 0 0 39840 72 0 0 25 0 1 0 1842350922 57548800 12980 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 14050 12980 145 145 0 13905 0
[pid=22148] vsize: 56200
Current children cumulated CPU time (s) 399.12
Current children cumulated vsize (Kb) 58324

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 13558 0 0 0 40836 74 0 0 25 0 1 0 1842350922 58335232 13174 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 14242 13174 145 145 0 14097 0
[pid=22148] vsize: 56968
Current children cumulated CPU time (s) 409.1
Current children cumulated vsize (Kb) 59092

[startup+420.041 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 13667 0 0 0 41834 76 0 0 25 0 1 0 1842350922 58777600 13283 4294967295 134512640 135094434 3221224448 3221223096 134558037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 14350 13283 145 145 0 14205 0
[pid=22148] vsize: 57400
Current children cumulated CPU time (s) 419.1
Current children cumulated vsize (Kb) 59524

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 13879 0 0 0 42830 77 0 0 25 0 1 0 1842350922 59641856 13495 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 14561 13495 145 145 0 14416 0
[pid=22148] vsize: 58244
Current children cumulated CPU time (s) 429.07
Current children cumulated vsize (Kb) 60368

[startup+440.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 14102 0 0 0 43827 79 0 0 25 0 1 0 1842350922 60551168 13718 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 14783 13718 145 145 0 14638 0
[pid=22148] vsize: 59132
Current children cumulated CPU time (s) 439.06
Current children cumulated vsize (Kb) 61256

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 14346 0 0 0 44823 81 0 0 25 0 1 0 1842350922 61546496 13962 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 15026 13962 145 145 0 14881 0
[pid=22148] vsize: 60104
Current children cumulated CPU time (s) 449.04
Current children cumulated vsize (Kb) 62228

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 14603 0 0 0 45819 84 0 0 25 0 1 0 1842350922 62590976 14219 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 15281 14219 145 145 0 15136 0
[pid=22148] vsize: 61124
Current children cumulated CPU time (s) 459.03
Current children cumulated vsize (Kb) 63248

[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 14844 0 0 0 46815 85 0 0 25 0 1 0 1842350922 63574016 14460 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 15521 14460 145 145 0 15376 0
[pid=22148] vsize: 62084
Current children cumulated CPU time (s) 469
Current children cumulated vsize (Kb) 64208

[startup+480.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15039 0 0 0 47813 86 0 0 25 0 1 0 1842350922 64368640 14655 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 15715 14655 145 145 0 15570 0
[pid=22148] vsize: 62860
Current children cumulated CPU time (s) 478.99
Current children cumulated vsize (Kb) 64984

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15130 0 0 0 48812 86 0 0 25 0 1 0 1842350922 64745472 14746 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 15807 14746 145 145 0 15662 0
[pid=22148] vsize: 63228
Current children cumulated CPU time (s) 488.98
Current children cumulated vsize (Kb) 65352

[startup+500.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15242 0 0 0 49810 87 0 0 25 0 1 0 1842350922 65196032 14858 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 15917 14858 145 145 0 15772 0
[pid=22148] vsize: 63668
Current children cumulated CPU time (s) 498.97
Current children cumulated vsize (Kb) 65792

[startup+510.048 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15362 0 0 0 50808 88 0 0 25 0 1 0 1842350922 65683456 14978 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16036 14978 145 145 0 15891 0
[pid=22148] vsize: 64144
Current children cumulated CPU time (s) 508.96
Current children cumulated vsize (Kb) 66268

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15489 0 0 0 51805 89 0 0 25 0 1 0 1842350922 66199552 15105 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16162 15105 145 145 0 16017 0
[pid=22148] vsize: 64648
Current children cumulated CPU time (s) 518.94
Current children cumulated vsize (Kb) 66772

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15589 0 0 0 52804 90 0 0 25 0 1 0 1842350922 66600960 15205 4294967295 134512640 135094434 3221224448 3221223072 134562131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16260 15205 145 145 0 16115 0
[pid=22148] vsize: 65040
Current children cumulated CPU time (s) 528.94
Current children cumulated vsize (Kb) 67164

[startup+540.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15670 0 0 0 53803 91 0 0 25 0 1 0 1842350922 66924544 15286 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16339 15286 145 145 0 16194 0
[pid=22148] vsize: 65356
Current children cumulated CPU time (s) 538.94
Current children cumulated vsize (Kb) 67480

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15759 0 0 0 54801 92 0 0 25 0 1 0 1842350922 67280896 15375 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 16426 15375 145 145 0 16281 0
[pid=22148] vsize: 65704
Current children cumulated CPU time (s) 548.93
Current children cumulated vsize (Kb) 67828

[startup+560.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 15926 0 0 0 55798 93 0 0 25 0 1 0 1842350922 67960832 15542 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16592 15542 145 145 0 16447 0
[pid=22148] vsize: 66368
Current children cumulated CPU time (s) 558.91
Current children cumulated vsize (Kb) 68492

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16037 0 0 0 56796 94 0 0 25 0 1 0 1842350922 68411392 15653 4294967295 134512640 135094434 3221224448 3221223104 134557987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16702 15653 145 145 0 16557 0
[pid=22148] vsize: 66808
Current children cumulated CPU time (s) 568.9
Current children cumulated vsize (Kb) 68932

[startup+580.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16174 0 0 0 57795 95 0 0 25 0 1 0 1842350922 68968448 15790 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16838 15790 145 145 0 16693 0
[pid=22148] vsize: 67352
Current children cumulated CPU time (s) 578.9
Current children cumulated vsize (Kb) 69476

[startup+590.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16260 0 0 0 58794 95 0 0 25 0 1 0 1842350922 69312512 15876 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 16922 15876 145 145 0 16777 0
[pid=22148] vsize: 67688
Current children cumulated CPU time (s) 588.89
Current children cumulated vsize (Kb) 69812

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16396 0 0 0 59792 96 0 0 25 0 1 0 1842350922 69865472 16012 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17057 16012 145 145 0 16912 0
[pid=22148] vsize: 68228
Current children cumulated CPU time (s) 598.88
Current children cumulated vsize (Kb) 70352

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16569 0 0 0 60790 97 0 0 25 0 1 0 1842350922 70569984 16185 4294967295 134512640 135094434 3221224448 3221223120 134555323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17229 16185 145 145 0 17084 0
[pid=22148] vsize: 68916
Current children cumulated CPU time (s) 608.87
Current children cumulated vsize (Kb) 71040

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16740 0 0 0 61787 98 0 0 25 0 1 0 1842350922 71258112 16356 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17397 16356 145 145 0 17252 0
[pid=22148] vsize: 69588
Current children cumulated CPU time (s) 618.85
Current children cumulated vsize (Kb) 71712

[startup+630.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 16919 0 0 0 62786 99 0 0 25 0 1 0 1842350922 71987200 16535 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17575 16535 145 145 0 17430 0
[pid=22148] vsize: 70300
Current children cumulated CPU time (s) 628.85
Current children cumulated vsize (Kb) 72424

[startup+640.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17112 0 0 0 63783 100 0 0 25 0 1 0 1842350922 72773632 16728 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17767 16728 145 145 0 17622 0
[pid=22148] vsize: 71068
Current children cumulated CPU time (s) 638.83
Current children cumulated vsize (Kb) 73192

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17266 0 0 0 64780 101 0 0 25 0 1 0 1842350922 73400320 16882 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 17920 16882 145 145 0 17775 0
[pid=22148] vsize: 71680
Current children cumulated CPU time (s) 648.81
Current children cumulated vsize (Kb) 73804

[startup+660.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17429 0 0 0 65777 102 0 0 25 0 1 0 1842350922 74067968 17045 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18083 17045 145 145 0 17938 0
[pid=22148] vsize: 72332
Current children cumulated CPU time (s) 658.79
Current children cumulated vsize (Kb) 74456

[startup+670.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17599 0 0 0 66775 104 0 0 25 0 1 0 1842350922 74760192 17215 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18252 17215 145 145 0 18107 0
[pid=22148] vsize: 73008
Current children cumulated CPU time (s) 668.79
Current children cumulated vsize (Kb) 75132

[startup+680.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17766 0 0 0 67772 105 0 0 25 0 1 0 1842350922 75440128 17382 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18418 17382 145 145 0 18273 0
[pid=22148] vsize: 73672
Current children cumulated CPU time (s) 678.77
Current children cumulated vsize (Kb) 75796

[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 17938 0 0 0 68769 106 0 0 25 0 1 0 1842350922 76136448 17554 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 18588 17554 145 145 0 18443 0
[pid=22148] vsize: 74352
Current children cumulated CPU time (s) 688.75
Current children cumulated vsize (Kb) 76476

[startup+700.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18026 0 0 0 69767 107 0 0 25 0 1 0 1842350922 76492800 17642 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18675 17642 145 145 0 18530 0
[pid=22148] vsize: 74700
Current children cumulated CPU time (s) 698.74
Current children cumulated vsize (Kb) 76824

[startup+710.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18102 0 0 0 70766 107 0 0 25 0 1 0 1842350922 76795904 17718 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18749 17718 145 145 0 18604 0
[pid=22148] vsize: 74996
Current children cumulated CPU time (s) 708.73
Current children cumulated vsize (Kb) 77120

[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18181 0 0 0 71764 108 0 0 25 0 1 0 1842350922 77115392 17797 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18827 17797 145 145 0 18682 0
[pid=22148] vsize: 75308
Current children cumulated CPU time (s) 718.72
Current children cumulated vsize (Kb) 77432

[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18266 0 0 0 72763 109 0 0 25 0 1 0 1842350922 77455360 17882 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18910 17882 145 145 0 18765 0
[pid=22148] vsize: 75640
Current children cumulated CPU time (s) 728.72
Current children cumulated vsize (Kb) 77764

[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18348 0 0 0 73762 109 0 0 25 0 1 0 1842350922 77799424 17964 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 18994 17964 145 145 0 18849 0
[pid=22148] vsize: 75976
Current children cumulated CPU time (s) 738.71
Current children cumulated vsize (Kb) 78100

[startup+750.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18456 0 0 0 74761 110 0 0 25 0 1 0 1842350922 78229504 18072 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19099 18072 145 145 0 18954 0
[pid=22148] vsize: 76396
Current children cumulated CPU time (s) 748.71
Current children cumulated vsize (Kb) 78520

[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18547 0 0 0 75760 111 0 0 25 0 1 0 1842350922 78598144 18163 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19189 18163 145 145 0 19044 0
[pid=22148] vsize: 76756
Current children cumulated CPU time (s) 758.71
Current children cumulated vsize (Kb) 78880

[startup+770.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18604 0 0 0 76759 111 0 0 25 0 1 0 1842350922 78823424 18220 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19244 18220 145 145 0 19099 0
[pid=22148] vsize: 76976
Current children cumulated CPU time (s) 768.7
Current children cumulated vsize (Kb) 79100

[startup+780.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18682 0 0 0 77758 111 0 0 25 0 1 0 1842350922 79138816 18298 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19321 18298 145 145 0 19176 0
[pid=22148] vsize: 77284
Current children cumulated CPU time (s) 778.69
Current children cumulated vsize (Kb) 79408

[startup+790.069 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18752 0 0 0 78757 112 0 0 25 0 1 0 1842350922 79417344 18368 4294967295 134512640 135094434 3221224448 3221223072 134557630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19389 18368 145 145 0 19244 0
[pid=22148] vsize: 77556
Current children cumulated CPU time (s) 788.69
Current children cumulated vsize (Kb) 79680

[startup+800.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18833 0 0 0 79755 112 0 0 25 0 1 0 1842350922 79757312 18449 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19472 18449 145 145 0 19327 0
[pid=22148] vsize: 77888
Current children cumulated CPU time (s) 798.67
Current children cumulated vsize (Kb) 80012

[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18909 0 0 0 80754 113 0 0 25 0 1 0 1842350922 80584704 18525 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19674 18525 145 145 0 19529 0
[pid=22148] vsize: 78696
Current children cumulated CPU time (s) 808.67
Current children cumulated vsize (Kb) 80820

[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 18995 0 0 0 81753 113 0 0 25 0 1 0 1842350922 80928768 18611 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19758 18611 145 145 0 19613 0
[pid=22148] vsize: 79032
Current children cumulated CPU time (s) 818.66
Current children cumulated vsize (Kb) 81156

[startup+830.074 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19082 0 0 0 82751 114 0 0 25 0 1 0 1842350922 81285120 18698 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19845 18698 145 145 0 19700 0
[pid=22148] vsize: 79380
Current children cumulated CPU time (s) 828.65
Current children cumulated vsize (Kb) 81504

[startup+840.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19167 0 0 0 83750 114 0 0 25 0 1 0 1842350922 81625088 18783 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 19928 18783 145 145 0 19783 0
[pid=22148] vsize: 79712
Current children cumulated CPU time (s) 838.64
Current children cumulated vsize (Kb) 81836

[startup+850.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19245 0 0 0 84750 115 0 0 25 0 1 0 1842350922 81960960 18861 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20010 18861 145 145 0 19865 0
[pid=22148] vsize: 80040
Current children cumulated CPU time (s) 848.65
Current children cumulated vsize (Kb) 82164

[startup+860.076 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19330 0 0 0 85748 115 0 0 25 0 1 0 1842350922 82296832 18946 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20092 18946 145 145 0 19947 0
[pid=22148] vsize: 80368
Current children cumulated CPU time (s) 858.63
Current children cumulated vsize (Kb) 82492

[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19405 0 0 0 86747 116 0 0 25 0 1 0 1842350922 82599936 19021 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20166 19021 145 145 0 20021 0
[pid=22148] vsize: 80664
Current children cumulated CPU time (s) 868.63
Current children cumulated vsize (Kb) 82788

[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19469 0 0 0 87747 116 0 0 25 0 1 0 1842350922 82857984 19085 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20229 19085 145 145 0 20084 0
[pid=22148] vsize: 80916
Current children cumulated CPU time (s) 878.63
Current children cumulated vsize (Kb) 83040

[startup+890.079 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19551 0 0 0 88745 117 0 0 25 0 1 0 1842350922 83193856 19167 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20311 19167 145 145 0 20166 0
[pid=22148] vsize: 81244
Current children cumulated CPU time (s) 888.62
Current children cumulated vsize (Kb) 83368

[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19683 0 0 0 89744 118 0 0 25 0 1 0 1842350922 83734528 19299 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20443 19299 145 145 0 20298 0
[pid=22148] vsize: 81772
Current children cumulated CPU time (s) 898.62
Current children cumulated vsize (Kb) 83896

[startup+910.082 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19767 0 0 0 90743 118 0 0 25 0 1 0 1842350922 84078592 19383 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20527 19383 145 145 0 20382 0
[pid=22148] vsize: 82108
Current children cumulated CPU time (s) 908.61
Current children cumulated vsize (Kb) 84232

[startup+920.082 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19876 0 0 0 91742 119 0 0 25 0 1 0 1842350922 84520960 19492 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20635 19492 145 145 0 20490 0
[pid=22148] vsize: 82540
Current children cumulated CPU time (s) 918.61
Current children cumulated vsize (Kb) 84664

[startup+930.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 19982 0 0 0 92740 120 0 0 25 0 1 0 1842350922 84951040 19598 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20740 19598 145 145 0 20595 0
[pid=22148] vsize: 82960
Current children cumulated CPU time (s) 928.6
Current children cumulated vsize (Kb) 85084

[startup+940.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20093 0 0 0 93740 120 0 0 25 0 1 0 1842350922 85401600 19709 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20850 19709 145 145 0 20705 0
[pid=22148] vsize: 83400
Current children cumulated CPU time (s) 938.6
Current children cumulated vsize (Kb) 85524

[startup+950.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20199 0 0 0 94738 122 0 0 25 0 1 0 1842350922 85831680 19815 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 20955 19815 145 145 0 20810 0
[pid=22148] vsize: 83820
Current children cumulated CPU time (s) 948.6
Current children cumulated vsize (Kb) 85944

[startup+960.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20272 0 0 0 95736 122 0 0 25 0 1 0 1842350922 86147072 19888 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21032 19888 145 145 0 20887 0
[pid=22148] vsize: 84128
Current children cumulated CPU time (s) 958.58
Current children cumulated vsize (Kb) 86252

[startup+970.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20386 0 0 0 96735 123 0 0 25 0 1 0 1842350922 86605824 20002 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21144 20002 145 145 0 20999 0
[pid=22148] vsize: 84576
Current children cumulated CPU time (s) 968.58
Current children cumulated vsize (Kb) 86700

[startup+980.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20514 0 0 0 97733 123 0 0 25 0 1 0 1842350922 87126016 20130 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22148/statm): 21271 20130 145 145 0 21126 0
[pid=22148] vsize: 85084
Current children cumulated CPU time (s) 978.56
Current children cumulated vsize (Kb) 87208

[startup+990.088 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20609 0 0 0 98731 124 0 0 25 0 1 0 1842350922 87511040 20225 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21365 20225 145 145 0 21220 0
[pid=22148] vsize: 85460
Current children cumulated CPU time (s) 988.55
Current children cumulated vsize (Kb) 87584

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20733 0 0 0 99729 125 0 0 25 0 1 0 1842350922 88023040 20349 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21490 20349 145 145 0 21345 0
[pid=22148] vsize: 85960
Current children cumulated CPU time (s) 998.54
Current children cumulated vsize (Kb) 88084

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 20903 0 0 0 100726 126 0 0 25 0 1 0 1842350922 88707072 20519 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21657 20519 145 145 0 21512 0
[pid=22148] vsize: 86628
Current children cumulated CPU time (s) 1008.52
Current children cumulated vsize (Kb) 88752

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 21112 0 0 0 101722 127 0 0 25 0 1 0 1842350922 89559040 20728 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 21865 20728 145 145 0 21720 0
[pid=22148] vsize: 87460
Current children cumulated CPU time (s) 1018.49
Current children cumulated vsize (Kb) 89584

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 21346 0 0 0 102719 129 0 0 25 0 1 0 1842350922 90513408 20962 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 22098 20962 145 145 0 21953 0
[pid=22148] vsize: 88392
Current children cumulated CPU time (s) 1028.48
Current children cumulated vsize (Kb) 90516

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 21554 0 0 0 103716 130 0 0 25 0 1 0 1842350922 91361280 21170 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 22305 21170 145 145 0 22160 0
[pid=22148] vsize: 89220
Current children cumulated CPU time (s) 1038.46
Current children cumulated vsize (Kb) 91344

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.98 1/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) T 22144 22144 16528 0 -1 0 21780 0 0 0 104713 132 0 0 25 0 1 0 1842350922 92286976 21396 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/22148/statm): 22531 21396 145 145 0 22386 0
[pid=22148] vsize: 90124
Current children cumulated CPU time (s) 1048.45
Current children cumulated vsize (Kb) 92248

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 22044 0 0 0 105708 134 0 0 25 0 1 0 1842350922 93364224 21660 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 22794 21660 145 145 0 22649 0
[pid=22148] vsize: 91176
Current children cumulated CPU time (s) 1058.42
Current children cumulated vsize (Kb) 93300

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 22300 0 0 0 106705 135 0 0 25 0 1 0 1842350922 94408704 21916 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 23049 21916 145 145 0 22904 0
[pid=22148] vsize: 92196
Current children cumulated CPU time (s) 1068.4
Current children cumulated vsize (Kb) 94320

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 22524 0 0 0 107701 137 0 0 25 0 1 0 1842350922 95322112 22140 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 23272 22140 145 145 0 23127 0
[pid=22148] vsize: 93088
Current children cumulated CPU time (s) 1078.38
Current children cumulated vsize (Kb) 95212

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 22718 0 0 0 108698 138 0 0 25 0 1 0 1842350922 96116736 22334 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 23466 22334 145 145 0 23321 0
[pid=22148] vsize: 93864
Current children cumulated CPU time (s) 1088.36
Current children cumulated vsize (Kb) 95988

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 22932 0 0 0 109695 140 0 0 25 0 1 0 1842350922 96989184 22548 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 23679 22548 145 145 0 23534 0
[pid=22148] vsize: 94716
Current children cumulated CPU time (s) 1098.35
Current children cumulated vsize (Kb) 96840

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 23147 0 0 0 110693 142 0 0 25 0 1 0 1842350922 97865728 22763 4294967295 134512640 135094434 3221224448 3221223040 134557369 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 23893 22763 145 145 0 23748 0
[pid=22148] vsize: 95572
Current children cumulated CPU time (s) 1108.35
Current children cumulated vsize (Kb) 97696

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 23367 0 0 0 111690 144 0 0 25 0 1 0 1842350922 98766848 22983 4294967295 134512640 135094434 3221224448 3221223040 134556906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 24113 22983 145 145 0 23968 0
[pid=22148] vsize: 96452
Current children cumulated CPU time (s) 1118.34
Current children cumulated vsize (Kb) 98576

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 23591 0 0 0 112687 145 0 0 25 0 1 0 1842350922 99680256 23207 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 24336 23207 145 145 0 24191 0
[pid=22148] vsize: 97344
Current children cumulated CPU time (s) 1128.32
Current children cumulated vsize (Kb) 99468

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 23846 0 0 0 113684 146 0 0 25 0 1 0 1842350922 100720640 23462 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 24590 23462 145 145 0 24445 0
[pid=22148] vsize: 98360
Current children cumulated CPU time (s) 1138.3
Current children cumulated vsize (Kb) 100484

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 24095 0 0 0 114681 147 0 0 25 0 1 0 1842350922 101740544 23711 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 24839 23711 145 145 0 24694 0
[pid=22148] vsize: 99356
Current children cumulated CPU time (s) 1148.28
Current children cumulated vsize (Kb) 101480

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 24340 0 0 0 115678 149 0 0 25 0 1 0 1842350922 102739968 23956 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 25083 23956 145 145 0 24938 0
[pid=22148] vsize: 100332
Current children cumulated CPU time (s) 1158.27
Current children cumulated vsize (Kb) 102456

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 24588 0 0 0 116674 150 0 0 25 0 1 0 1842350922 103751680 24204 4294967295 134512640 135094434 3221224448 3221223040 134557253 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 25330 24204 145 145 0 25185 0
[pid=22148] vsize: 101320
Current children cumulated CPU time (s) 1168.24
Current children cumulated vsize (Kb) 103444

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 24842 0 0 0 117670 152 0 0 25 0 1 0 1842350922 104792064 24458 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 25584 24458 145 145 0 25439 0
[pid=22148] vsize: 102336
Current children cumulated CPU time (s) 1178.22
Current children cumulated vsize (Kb) 104460

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 25036 0 0 0 118668 153 0 0 25 0 1 0 1842350922 105578496 24652 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 25776 24652 145 145 0 25631 0
[pid=22148] vsize: 103104
Current children cumulated CPU time (s) 1188.21
Current children cumulated vsize (Kb) 105228

[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 25251 0 0 0 119665 154 0 0 25 0 1 0 1842350922 106455040 24867 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 25990 24867 145 145 0 25845 0
[pid=22148] vsize: 103960
Current children cumulated CPU time (s) 1198.19
Current children cumulated vsize (Kb) 106084

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 25435 0 0 0 120662 155 0 0 25 0 1 0 1842350922 107204608 25051 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 26173 25051 145 145 0 26028 0
[pid=22148] vsize: 104692
Current children cumulated CPU time (s) 1208.17
Current children cumulated vsize (Kb) 106816



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 22148
Raw data (/proc/22144/stat): 22144 (minisat+_script) S 22143 22144 16528 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1842350917 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/22144/statm): 531 226 485 147 0 384 0
[pid=22144] vsize: 2124
Raw data (/proc/22148/stat): 22148 (minisat+_64-bit) R 22144 22144 16528 0 -1 0 25435 0 0 0 120662 155 0 0 25 0 1 0 1842350922 107204608 25051 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22148/statm): 26173 25051 145 145 0 26028 0
[pid=22148] vsize: 104692
Current children cumulated CPU time (s) 1208.17
Current children cumulated vsize (Kb) 106816

Sending SIGTERM to -22144
Sleeping 2 seconds
One traced child (pid=22144) ended because it received signal 15 (SIGTERM)
One traced child (pid=22148) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.23
CPU user time (s): 1206.63
CPU system time (s): 1.60376
CPU usage (%): 99.8403
Max. virtual memory (cumulated for all children) (Kb): 106816

Verifier Data

ERROR: no interpretation found !