| Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod008.opb |
| MD5SUM | fbdb3cf321a85412feefcaac30780520 |
| Bench Category | optimization, small integers (OPTSMALLINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 361 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 319 |
| Biggest coefficient in the objective function | 87 |
| Number of bits for the biggest coefficient in the objective function | 7 |
| Sum of the numbers in the objective function | 23554 |
| Number of bits of the sum of numbers in the objective function | 15 |
| Biggest number in a constraint | 22000 |
| Number of bits of the biggest number in a constraint | 15 |
| Biggest sum of numbers in a constraint | 1027256 |
| Number of bits of the biggest sum of numbers | 20 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1195.07 |
| Number of variables | 319 |
| Total number of constraints | 325 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 319 |
| Number of constraints which are nor clauses,nor cardinality constraints | 6 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 231 |
LAUNCH ON wulflinc30 THE 2005-09-20 03:14:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3252 boxname=wulflinc30 idbench=908 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fbdb3cf321a85412feefcaac30780520 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb IDLAUNCH: 3252 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 867608 kB Buffers: 28600 kB Cached: 108756 kB SwapCached: 752 kB Active: 32860 kB Inactive: 107140 kB HighTotal: 131008 kB HighFree: 28252 kB LowTotal: 903652 kB LowFree: 839356 kB SwapTotal: 2097892 kB SwapFree: 2096620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 21384 kB Committed_AS: 64304 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:35:01 (client local time) WITH STATUS 10 IN 1208.68 SECONDS stats: 3252 7 1208.68 10
c Parsing PB file... c Converting 6 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): sss c ---[ 8]---> Adder-cost: 2481 maxlim: 21999 bits: 16/15 c ---[ 5]---> Adder-cost: 2052 maxlim: 4999 bits: 14/13 c ---[ 4]---> Adder-cost: 2306 maxlim: 11999 bits: 15/14 c ---[ 2]---> BDD-cost: 478 c ---[ 1]---> BDD-cost: 2553 c ---[ 0]---> Adder-cost: 1803 maxlim: 3999 bits: 13/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 62010 221290 | 20670 0 0 nan | 0.000 % | c | 100 | 62010 221290 | 22737 100 343 3.4 | 0.272 % | c | 251 | 62010 221290 | 25010 251 940 3.7 | 0.272 % | c | 477 | 62010 221290 | 27511 477 2129 4.5 | 0.272 % | c | 816 | 62010 221290 | 30262 816 14323 17.6 | 0.272 % | c | 1323 | 62010 221290 | 33289 1323 19211 14.5 | 0.272 % | c ============================================================================== c [1mFound solution: 1989[0m c ---[ 0]---> Sorter-cost:61666 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2068 | 212587 572921 | 70862 2068 31161 15.1 | 0.272 % | c | 2168 | 212587 572921 | 77948 2168 31706 14.6 | 0.044 % | c | 2318 | 212587 572921 | 85743 2318 33024 14.2 | 0.044 % | c | 2544 | 212587 572921 | 94317 2544 44942 17.7 | 0.044 % | c | 2881 | 212587 572921 | 103749 2881 48764 16.9 | 0.044 % | c | 3387 | 212587 572921 | 114123 3387 58430 17.3 | 0.044 % | c | 4146 | 212587 572921 | 125536 4146 66243 16.0 | 0.044 % | c | 5285 | 212587 572921 | 138089 5285 84457 16.0 | 0.044 % | c | 6993 | 212587 572921 | 151898 6993 111949 16.0 | 0.044 % | c | 9555 | 212587 572921 | 167088 9555 195934 20.5 | 0.044 % | c | 13401 | 212587 572921 | 183797 13401 357669 26.7 | 0.044 % | c ============================================================================== c [1mFound solution: 1974[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 13769 | 212607 573161 | 70869 13769 383633 27.9 | 0.044 % | c | 13869 | 212607 573161 | 77955 13869 384775 27.7 | 0.046 % | c | 14021 | 212607 573161 | 85751 14021 385869 27.5 | 0.046 % | c | 14246 | 212607 573161 | 94326 14246 394337 27.7 | 0.046 % | c ============================================================================== c [1mFound solution: 814[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14260 | 212681 573330 | 70893 14260 394825 27.7 | 0.046 % | c ============================================================================== c [1mFound solution: 574[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14279 | 212709 573397 | 70903 14279 395338 27.7 | 0.046 % | c ============================================================================== c [1mFound solution: 573[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14286 | 213333 575013 | 71111 14286 396113 27.7 | 0.046 % | c | 14391 | 213333 575013 | 78222 14391 410775 28.5 | 0.050 % | c | 14541 | 213333 575013 | 86044 14541 418766 28.8 | 0.050 % | c | 14767 | 213333 575013 | 94648 14767 425049 28.8 | 0.050 % | c | 15104 | 213250 574823 | 104113 15041 440754 29.3 | 0.082 % | c | 15610 | 213250 574823 | 114524 15547 456423 29.4 | 0.082 % | c | 16371 | 213250 574823 | 125977 16308 475439 29.2 | 0.082 % | c ============================================================================== c [1mFound solution: 548[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16771 | 213076 574533 | 71025 16590 503647 30.4 | 0.082 % | c | 16873 | 213076 574533 | 78127 16692 520097 31.2 | 0.158 % | c | 17023 | 213076 574533 | 85940 16842 530977 31.5 | 0.158 % | c | 17248 | 213076 574533 | 94534 17067 535357 31.4 | 0.158 % | c | 17585 | 212948 574238 | 103987 17398 545681 31.4 | 0.217 % | c | 18092 | 212758 573802 | 114386 17829 590918 33.1 | 0.297 % | c | 18851 | 212367 572913 | 125825 18400 651840 35.4 | 0.464 % | c | 19991 | 212090 572277 | 138407 19470 687672 35.3 | 0.589 % | c ============================================================================== c [1mFound solution: 525[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20564 | 212094 572286 | 70698 20043 725393 36.2 | 0.589 % | c | 20664 | 212094 572286 | 77767 20143 730456 36.3 | 0.591 % | c | 20815 | 212094 572286 | 85544 20294 776161 38.2 | 0.591 % | c | 21040 | 212094 572286 | 94099 20519 805956 39.3 | 0.591 % | c | 21381 | 212074 572241 | 103508 20858 857655 41.1 | 0.598 % | c | 21887 | 212074 572241 | 113859 21364 927987 43.4 | 0.598 % | c ============================================================================== c [1mFound solution: 389[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22374 | 212090 572280 | 70696 21851 967074 44.3 | 0.598 % | c | 22476 | 212090 572280 | 77765 21953 972904 44.3 | 0.600 % | c | 22627 | 212090 572280 | 85542 22104 1012989 45.8 | 0.600 % | c | 22852 | 212090 572280 | 94096 22329 1051720 47.1 | 0.600 % | c | 23190 | 212090 572280 | 103506 22667 1072607 47.3 | 0.600 % | c | 23696 | 212090 572280 | 113856 23173 1121981 48.4 | 0.600 % | c | 24455 | 212090 572280 | 125242 23932 1188663 49.7 | 0.600 % | c | 25596 | 212090 572280 | 137766 25073 1311227 52.3 | 0.600 % | c | 27308 | 211704 571405 | 151543 26765 1500814 56.1 | 0.759 % | c | 29871 | 211704 571405 | 166697 29328 2469277 84.2 | 0.759 % | c | 33716 | 211704 571405 | 183367 33173 3164018 95.4 | 0.759 % | c | 39483 | 211084 569990 | 201703 38873 4866988 125.2 | 1.036 % | c | 48135 | 210928 569631 | 221874 47496 6207615 130.7 | 1.110 % | c | 61110 | 210871 569502 | 244061 60467 7966433 131.7 | 1.134 % | c | 80574 | 210871 569502 | 268467 79931 10789561 135.0 | 1.134 % | c ============================================================================== c [1mFound solution: 385[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 93507 | 210875 569512 | 70291 92864 12122456 130.5 | 1.134 % | c | 93607 | 210875 569512 | 77320 26188 1518346 58.0 | 1.136 % | c | 93758 | 210875 569512 | 85052 26339 1522964 57.8 | 1.136 % | c | 93983 | 210875 569512 | 93557 26564 1531296 57.6 | 1.136 % | c | 94320 | 210875 569512 | 102913 26901 1590344 59.1 | 1.136 % | c | 94826 | 210875 569512 | 113204 27407 1653992 60.3 | 1.136 % | c | 95589 | 210813 569370 | 124524 28168 1742947 61.9 | 1.163 % | c | 96733 | 210813 569370 | 136977 29312 1979284 67.5 | 1.163 % | c | 98441 | 210813 569370 | 150675 31020 2403707 77.5 | 1.163 % | c c *** TERMINATED *** s SATISFIABLE v -C2_0x2e__bit0 -C3_0x2e__bit0 -C4_0x2e__bit0 -C5_0x2e__bit0 -C6_0x2e__bit0 -C7_0x2e__bit0 -C8_0x2e__bit0 -C9_0x2e__bit0 -C10_0x2e__bit0 -C11_0x2e__bit0 -C12_0x2e__bit0 -C13_0x2e__bit0 -C14_0x2e__bit0 -C15_0x2e__bit0 -C16_0x2e__bit0 -C17_0x2e__bit0 -C18_0x2e__bit0 -C19_0x2e__bit0 -C20_0x2e__bit0 -C21_0x2e__bit0 -C22_0x2e__bit0 -C23_0x2e__bit0 -C24_0x2e__bit0 -C25_0x2e__bit0 -C26_0x2e__bit0 -C27_0x2e__bit0 -C28_0x2e__bit0 C29_0x2e__bit0 -C30_0x2e__bit0 -C31_0x2e__bit0 -C32_0x2e__bit0 -C33_0x2e__bit0 -C34_0x2e__bit0 -C35_0x2e__bit0 -C36_0x2e__bit0 -C37_0x2e__bit0 -C38_0x2e__bit0 -C39_0x2e__bit0 -C40_0x2e__bit0 -C41_0x2e__bit0 -C42_0x2e__bit0 -C43_0x2e__bit0 -C44_0x2e__bit0 -C45_0x2e__bit0 -C46_0x2e__bit0 -C47_0x2e__bit0 -C48_0x2e__bit0 -C49_0x2e__bit0 -C50_0x2e__bit0 -C51_0x2e__bit0 -C52_0x2e__bit0 -C53_0x2e__bit0 -C54_0x2e__bit0 -C55_0x2e__bit0 -C56_0x2e__bit0 -C57_0x2e__bit0 -C58_0x2e__bit0 -C59_0x2e__bit0 -C60_0x2e__bit0 -C61_0x2e__bit0 -C62_0x2e__bit0 -C63_0x2e__bit0 -C64_0x2e__bit0 -C65_0x2e__bit0 -C66_0x2e__bit0 -C67_0x2e__bit0 -C68_0x2e__bit0 -C69_0x2e__bit0 -C70_0x2e__bit0 -C71_0x2e__bit0 -C72_0x2e__bit0 -C73_0x2e__bit0 -C74_0x2e__bit0 -C75_0x2e__bit0 -C76_0x2e__bit0 -C77_0x2e__bit0 -C78_0x2e__bit0 -C79_0x2e__bit0 -C80_0x2e__bit0 -C81_0x2e__bit0 -C82_0x2e__bit0 -C83_0x2e__bit0 -C84_0x2e__bit0 -C85_0x2e__bit0 -C86_0x2e__bit0 -C87_0x2e__bit0 -C88_0x2e__bit0 -C89_0x2e__bit0 -C90_0x2e__bit0 -C91_0x2e__bit0 -C92_0x2e__bit0 -C93_0x2e__bit0 -C94_0x2e__bit0 -C95_0x2e__bit0 -C96_0x2e__bit0 -C97_0x2e__bit0 -C98_0x2e__bit0 -C99_0x2e__bit0 -C100_0x2e__bit0 -C101_0x2e__bit0 -C102_0x2e__bit0 -C103_0x2e__bit0 -C104_0x2e__bit0 -C105_0x2e__bit0 -C106_0x2e__bit0 -C107_0x2e__bit0 -C108_0x2e__bit0 -C109_0x2e__bit0 -C110_0x2e__bit0 -C111_0x2e__bit0 -C112_0x2e__bit0 -C113_0x2e__bit0 -C114_0x2e__bit0 -C115_0x2e__bit0 -C116_0x2e__bit0 -C117_0x2e__bit0 -C118_0x2e__bit0 -C119_0x2e__bit0 -C120_0x2e__bit0 -C121_0x2e__bit0 -C122_0x2e__bit0 -C123_0x2e__bit0 -C124_0x2e__bit0 -C125_0x2e__bit0 -C126_0x2e__bit0 -C127_0x2e__bit0 -C128_0x2e__bit0 -C129_0x2e__bit0 -C130_0x2e__bit0 -C131_0x2e__bit0 -C132_0x2e__bit0 -C133_0x2e__bit0 -C134_0x2e__bit0 -C135_0x2e__bit0 -C136_0x2e__bit0 -C137_0x2e__bit0 -C138_0x2e__bit0 -C139_0x2e__bit0 -C140_0x2e__bit0 -C141_0x2e__bit0 -C142_0x2e__bit0 -C143_0x2e__bit0 -C144_0x2e__bit0 -C145_0x2e__bit0 -C146_0x2e__bit0 -C147_0x2e__bit0 -C148_0x2e__bit0 -C149_0x2e__bit0 -C150_0x2e__bit0 -C151_0x2e__bit0 -C152_0x2e__bit0 -C153_0x2e__bit0 -C154_0x2e__bit0 -C155_0x2e__bit0 -C156_0x2e__bit0 -C157_0x2e__bit0 -C158_0x2e__bit0 -C159_0x2e__bit0 -C160_0x2e__bit0 -C161_0x2e__bit0 -C162_0x2e__bit0 -C163_0x2e__bit0 -C164_0x2e__bit0 -C165_0x2e__bit0 -C166_0x2e__bit0 -C167_0x2e__bit0 -C168_0x2e__bit0 -C169_0x2e__bit0 -C170_0x2e__bit0 -C171_0x2e__bit0 -C172_0x2e__bit0 -C173_0x2e__bit0 -C174_0x2e__bit0 -C175_0x2e__bit0 -C176_0x2e__bit0 -C177_0x2e__bit0 -C178_0x2e__bit0 -C179_0x2e__bit0 -C180_0x2e__bit0 -C181_0x2e__bit0 -C182_0x2e__bit0 -C183_0x2e__bit0 -C184_0x2e__bit0 -C185_0x2e__bit0 -C186_0x2e__bit0 -C187_0x2e__bit0 -C188_0x2e__bit0 -C189_0x2e__bit0 -C190_0x2e__bit0 -C191_0x2e__bit0 -C192_0x2e__bit0 -C193_0x2e__bit0 -C194_0x2e__bit0 -C195_0x2e__bit0 -C196_0x2e__bit0 -C197_0x2e__bit0 -C198_0x2e__bit0 -C199_0x2e__bit0 -C200_0x2e__bit0 -C201_0x2e__bit0 -C202_0x2e__bit0 -C203_0x2e__bit0 -C204_0x2e__bit0 -C205_0x2e__bit0 -C206_0x2e__bit0 -C207_0x2e__bit0 -C208_0x2e__bit0 -C209_0x2e__bit0 -C210_0x2e__bit0 -C211_0x2e__bit0 -C212_0x2e__bit0 C213_0x2e__bit0 -C214_0x2e__bit0 -C215_0x2e__bit0 C216_0x2e__bit0 -C217_0x2e__bit0 -C218_0x2e__bit0 -C219_0x2e__bit0 -C220_0x2e__bit0 -C221_0x2e__bit0 -C222_0x2e__bit0 -C223_0x2e__bit0 -C224_0x2e__bit0 -C225_0x2e__bit0 -C226_0x2e__bit0 -C227_0x2e__bit0 -C228_0x2e__bit0 -C229_0x2e__bit0 -C230_0x2e__bit0 C231_0x2e__bit0 -C232_0x2e__bit0 -C233_0x2e__bit0 -C234_0x2e__bit0 -C235_0x2e__bit0 -C236_0x2e__bit0 -C237_0x2e__bit0 -C238_0x2e__bit0 -C239_0x2e__bit0 -C240_0x2e__bit0 -C241_0x2e__bit0 -C242_0x2e__bit0 -C243_0x2e__bit0 -C244_0x2e__bit0 -C245_0x2e__bit0 -C246_0x2e__bit0 -
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/3266/stat): 3266 (minisat+_script) R 3265 3266 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855203886 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/3266/statm): 174 3 169 147 0 27 0 [pid=3266] 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=3267 New process pid=3268 New process pid=3269 execve syscall for /bin/sed executable One traced child (pid=3268) 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=3269) exited with status: 0 One traced child (pid=3267) exited with status: 0 New process pid=3270 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-mod008.opb [startup+10.0034 s] Raw data (loadavg): 0.98 0.98 0.72 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 4707 0 0 0 966 15 0 0 25 0 1 0 1855203891 5906432 1286 4294967295 134512640 135094434 3221224432 3221221956 134676380 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 1442 1286 145 145 0 1297 0 [pid=3270] vsize: 5768 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 7892 [startup+20.0042 s] Raw data (loadavg): 0.98 0.98 0.72 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 9625 0 0 0 1928 33 0 0 25 0 1 0 1855203891 28651520 5736 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 6995 5736 145 145 0 6850 0 [pid=3270] vsize: 27980 Current children cumulated CPU time (s) 19.61 Current children cumulated vsize (Kb) 30104 [startup+30.006 s] Raw data (loadavg): 0.99 0.98 0.73 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 9680 0 0 0 2928 34 0 0 25 0 1 0 1855203891 28823552 5791 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 7037 5791 145 145 0 6892 0 [pid=3270] vsize: 28148 Current children cumulated CPU time (s) 29.62 Current children cumulated vsize (Kb) 30272 [startup+40.0068 s] Raw data (loadavg): 0.99 0.98 0.73 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 9815 0 0 0 3926 35 0 0 25 0 1 0 1855203891 29360128 5926 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 7168 5926 145 145 0 7023 0 [pid=3270] vsize: 28672 Current children cumulated CPU time (s) 39.61 Current children cumulated vsize (Kb) 30796 [startup+50.0086 s] Raw data (loadavg): 0.99 0.98 0.73 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 9973 0 0 0 4922 36 0 0 25 0 1 0 1855203891 29986816 6084 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7321 6084 145 145 0 7176 0 [pid=3270] vsize: 29284 Current children cumulated CPU time (s) 49.58 Current children cumulated vsize (Kb) 31408 [startup+60.0093 s] Raw data (loadavg): 0.99 0.98 0.73 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10242 0 0 0 5920 37 0 0 25 0 1 0 1855203891 30896128 6311 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7543 6311 145 145 0 7398 0 [pid=3270] vsize: 30172 Current children cumulated CPU time (s) 59.57 Current children cumulated vsize (Kb) 32296 [startup+70.0101 s] Raw data (loadavg): 0.99 0.98 0.74 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10264 0 0 0 6920 38 0 0 25 0 1 0 1855203891 30982144 6333 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7564 6333 145 145 0 7419 0 [pid=3270] vsize: 30256 Current children cumulated CPU time (s) 69.58 Current children cumulated vsize (Kb) 32380 [startup+80.0119 s] Raw data (loadavg): 0.99 0.98 0.74 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10309 0 0 0 7920 38 0 0 25 0 1 0 1855203891 31227904 6378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7624 6378 145 145 0 7479 0 [pid=3270] vsize: 30496 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 32620 [startup+90.0127 s] Raw data (loadavg): 0.99 0.98 0.74 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10424 0 0 0 8919 39 0 0 25 0 1 0 1855203891 31424512 6428 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7672 6428 145 145 0 7527 0 [pid=3270] vsize: 30688 Current children cumulated CPU time (s) 89.58 Current children cumulated vsize (Kb) 32812 [startup+100.013 s] Raw data (loadavg): 0.99 0.98 0.74 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10496 0 0 0 9918 40 0 0 25 0 1 0 1855203891 31723520 6500 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7745 6500 145 145 0 7600 0 [pid=3270] vsize: 30980 Current children cumulated CPU time (s) 99.58 Current children cumulated vsize (Kb) 33104 [startup+110.014 s] Raw data (loadavg): 0.99 0.98 0.74 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10587 0 0 0 10916 40 0 0 25 0 1 0 1855203891 32092160 6591 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 7835 6591 145 145 0 7690 0 [pid=3270] vsize: 31340 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 33464 [startup+120.015 s] Raw data (loadavg): 0.99 0.98 0.75 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 10849 0 0 0 11912 42 0 0 25 0 1 0 1855203891 32632832 6726 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 7967 6726 145 145 0 7822 0 [pid=3270] vsize: 31868 Current children cumulated CPU time (s) 119.54 Current children cumulated vsize (Kb) 33992 [startup+130.017 s] Raw data (loadavg): 0.99 0.98 0.75 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11014 0 0 0 12909 43 0 0 25 0 1 0 1855203891 33361920 6891 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8145 6891 145 145 0 8000 0 [pid=3270] vsize: 32580 Current children cumulated CPU time (s) 129.52 Current children cumulated vsize (Kb) 34704 [startup+140.018 s] Raw data (loadavg): 0.99 0.98 0.75 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11238 0 0 0 13905 45 0 0 25 0 1 0 1855203891 34009088 7051 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8303 7051 145 145 0 8158 0 [pid=3270] vsize: 33212 Current children cumulated CPU time (s) 139.5 Current children cumulated vsize (Kb) 35336 [startup+150.019 s] Raw data (loadavg): 0.99 0.98 0.75 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11293 0 0 0 14905 45 0 0 25 0 1 0 1855203891 34230272 7106 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8357 7106 145 145 0 8212 0 [pid=3270] vsize: 33428 Current children cumulated CPU time (s) 149.5 Current children cumulated vsize (Kb) 35552 [startup+160.02 s] Raw data (loadavg): 1.15 1.02 0.76 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11399 0 0 0 15903 47 0 0 25 0 1 0 1855203891 34660352 7212 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8462 7212 145 145 0 8317 0 [pid=3270] vsize: 33848 Current children cumulated CPU time (s) 159.5 Current children cumulated vsize (Kb) 35972 [startup+170.021 s] Raw data (loadavg): 1.12 1.02 0.77 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11463 0 0 0 16902 47 0 0 25 0 1 0 1855203891 34922496 7276 4294967295 134512640 135094434 3221224432 3221223056 134562131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8526 7276 145 145 0 8381 0 [pid=3270] vsize: 34104 Current children cumulated CPU time (s) 169.49 Current children cumulated vsize (Kb) 36228 [startup+180.022 s] Raw data (loadavg): 1.10 1.01 0.77 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11514 0 0 0 17902 47 0 0 25 0 1 0 1855203891 35090432 7327 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8567 7327 145 145 0 8422 0 [pid=3270] vsize: 34268 Current children cumulated CPU time (s) 179.49 Current children cumulated vsize (Kb) 36392 [startup+190.023 s] Raw data (loadavg): 1.09 1.01 0.77 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11687 0 0 0 18899 49 0 0 25 0 1 0 1855203891 35794944 7500 4294967295 134512640 135094434 3221224432 3221223164 134670016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8739 7500 145 145 0 8594 0 [pid=3270] vsize: 34956 Current children cumulated CPU time (s) 189.48 Current children cumulated vsize (Kb) 37080 [startup+200.023 s] Raw data (loadavg): 1.07 1.01 0.77 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 11896 0 0 0 19895 51 0 0 25 0 1 0 1855203891 36646912 7709 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 8947 7709 145 145 0 8802 0 [pid=3270] vsize: 35788 Current children cumulated CPU time (s) 199.46 Current children cumulated vsize (Kb) 37912 [startup+210.024 s] Raw data (loadavg): 1.06 1.01 0.77 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 12199 0 0 0 20892 52 0 0 25 0 1 0 1855203891 37883904 8012 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 9249 8012 145 145 0 9104 0 [pid=3270] vsize: 36996 Current children cumulated CPU time (s) 209.44 Current children cumulated vsize (Kb) 39120 [startup+220.025 s] Raw data (loadavg): 1.05 1.01 0.78 1/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) T 3266 3266 5245 0 -1 0 12680 0 0 0 21885 55 0 0 25 0 1 0 1855203891 39849984 8493 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/3270/statm): 9729 8493 145 145 0 9584 0 [pid=3270] vsize: 38916 Current children cumulated CPU time (s) 219.4 Current children cumulated vsize (Kb) 41040 [startup+230.026 s] Raw data (loadavg): 1.04 1.01 0.78 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 12884 0 0 0 22882 57 0 0 25 0 1 0 1855203891 40681472 8697 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 9932 8697 145 145 0 9787 0 [pid=3270] vsize: 39728 Current children cumulated CPU time (s) 229.39 Current children cumulated vsize (Kb) 41852 [startup+240.026 s] Raw data (loadavg): 1.04 1.01 0.78 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 13256 0 0 0 23875 60 0 0 25 0 1 0 1855203891 42201088 9069 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 10303 9069 145 145 0 10158 0 [pid=3270] vsize: 41212 Current children cumulated CPU time (s) 239.35 Current children cumulated vsize (Kb) 43336 [startup+250.028 s] Raw data (loadavg): 1.03 1.01 0.78 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 13392 0 0 0 24873 60 0 0 25 0 1 0 1855203891 42885120 9205 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 10470 9205 145 145 0 10325 0 [pid=3270] vsize: 41880 Current children cumulated CPU time (s) 249.33 Current children cumulated vsize (Kb) 44004 [startup+260.029 s] Raw data (loadavg): 1.03 1.01 0.78 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 13621 0 0 0 25870 61 0 0 25 0 1 0 1855203891 43814912 9434 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 10697 9434 145 145 0 10552 0 [pid=3270] vsize: 42788 Current children cumulated CPU time (s) 259.31 Current children cumulated vsize (Kb) 44912 [startup+270.029 s] Raw data (loadavg): 1.02 1.01 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 13914 0 0 0 26867 63 0 0 25 0 1 0 1855203891 45015040 9727 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 10990 9727 145 145 0 10845 0 [pid=3270] vsize: 43960 Current children cumulated CPU time (s) 269.3 Current children cumulated vsize (Kb) 46084 [startup+280.031 s] Raw data (loadavg): 1.02 1.00 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 14154 0 0 0 27863 65 0 0 25 0 1 0 1855203891 45993984 9967 4294967295 134512640 135094434 3221224432 3221223104 134555826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 11229 9967 145 145 0 11084 0 [pid=3270] vsize: 44916 Current children cumulated CPU time (s) 279.28 Current children cumulated vsize (Kb) 47040 [startup+290.031 s] Raw data (loadavg): 1.01 1.00 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 14441 0 0 0 28858 66 0 0 25 0 1 0 1855203891 47165440 10254 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 11515 10254 145 145 0 11370 0 [pid=3270] vsize: 46060 Current children cumulated CPU time (s) 289.24 Current children cumulated vsize (Kb) 48184 [startup+300.032 s] Raw data (loadavg): 1.01 1.00 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 14597 0 0 0 29857 67 0 0 25 0 1 0 1855203891 47804416 10410 4294967295 134512640 135094434 3221224432 3221223024 134557363 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 11671 10410 145 145 0 11526 0 [pid=3270] vsize: 46684 Current children cumulated CPU time (s) 299.24 Current children cumulated vsize (Kb) 48808 [startup+310.033 s] Raw data (loadavg): 1.01 1.00 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 14893 0 0 0 30853 69 0 0 25 0 1 0 1855203891 49004544 10706 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 11964 10706 145 145 0 11819 0 [pid=3270] vsize: 47856 Current children cumulated CPU time (s) 309.22 Current children cumulated vsize (Kb) 49980 [startup+320.034 s] Raw data (loadavg): 1.01 1.00 0.79 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 15095 0 0 0 31851 70 0 0 25 0 1 0 1855203891 49831936 10908 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 12166 10908 145 145 0 12021 0 [pid=3270] vsize: 48664 Current children cumulated CPU time (s) 319.21 Current children cumulated vsize (Kb) 50788 [startup+330.035 s] Raw data (loadavg): 1.01 1.00 0.80 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 15293 0 0 0 32848 72 0 0 25 0 1 0 1855203891 50634752 11106 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 12362 11106 145 145 0 12217 0 [pid=3270] vsize: 49448 Current children cumulated CPU time (s) 329.2 Current children cumulated vsize (Kb) 51572 [startup+340.035 s] Raw data (loadavg): 1.00 1.00 0.80 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 15505 0 0 0 33844 73 0 0 25 0 1 0 1855203891 51499008 11318 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 12573 11318 145 145 0 12428 0 [pid=3270] vsize: 50292 Current children cumulated CPU time (s) 339.17 Current children cumulated vsize (Kb) 52416 [startup+350.036 s] Raw data (loadavg): 1.00 1.00 0.80 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 15754 0 0 0 34839 76 0 0 25 0 1 0 1855203891 52510720 11567 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 12820 11567 145 145 0 12675 0 [pid=3270] vsize: 51280 Current children cumulated CPU time (s) 349.15 Current children cumulated vsize (Kb) 53404 [startup+360.037 s] Raw data (loadavg): 1.00 1.00 0.80 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 15908 0 0 0 35835 78 0 0 25 0 1 0 1855203891 53137408 11721 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 12973 11721 145 145 0 12828 0 [pid=3270] vsize: 51892 Current children cumulated CPU time (s) 359.13 Current children cumulated vsize (Kb) 54016 [startup+370.038 s] Raw data (loadavg): 1.00 1.00 0.80 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 16113 0 0 0 36833 79 0 0 25 0 1 0 1855203891 53972992 11926 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 13177 11926 145 145 0 13032 0 [pid=3270] vsize: 52708 Current children cumulated CPU time (s) 369.12 Current children cumulated vsize (Kb) 54832 [startup+380.038 s] Raw data (loadavg): 1.00 1.00 0.81 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 16325 0 0 0 37830 80 0 0 25 0 1 0 1855203891 54841344 12138 4294967295 134512640 135094434 3221224432 3221223024 134557275 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 13389 12138 145 145 0 13244 0 [pid=3270] vsize: 53556 Current children cumulated CPU time (s) 379.1 Current children cumulated vsize (Kb) 55680 [startup+390.039 s] Raw data (loadavg): 1.00 1.00 0.81 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 16479 0 0 0 38828 81 0 0 25 0 1 0 1855203891 55472128 12292 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 13543 12292 145 145 0 13398 0 [pid=3270] vsize: 54172 Current children cumulated CPU time (s) 389.09 Current children cumulated vsize (Kb) 56296 [startup+400.046 s] Raw data (loadavg): 1.00 1.00 0.81 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 16728 0 0 0 39825 83 0 0 25 0 1 0 1855203891 56479744 12541 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 13789 12541 145 145 0 13644 0 [pid=3270] vsize: 55156 Current children cumulated CPU time (s) 399.08 Current children cumulated vsize (Kb) 57280 [startup+410.047 s] Raw data (loadavg): 1.00 1.00 0.81 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 16970 0 0 0 40821 85 0 0 25 0 1 0 1855203891 57462784 12783 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 14029 12783 145 145 0 13884 0 [pid=3270] vsize: 56116 Current children cumulated CPU time (s) 409.06 Current children cumulated vsize (Kb) 58240 [startup+420.047 s] Raw data (loadavg): 1.00 1.00 0.81 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 17164 0 0 0 41818 85 0 0 25 0 1 0 1855203891 58253312 12977 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 14222 12977 145 145 0 14077 0 [pid=3270] vsize: 56888 Current children cumulated CPU time (s) 419.03 Current children cumulated vsize (Kb) 59012 [startup+430.048 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 17200 0 0 0 42818 86 0 0 25 0 1 0 1855203891 58396672 13013 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 14257 13013 145 145 0 14112 0 [pid=3270] vsize: 57028 Current children cumulated CPU time (s) 429.04 Current children cumulated vsize (Kb) 59152 [startup+440.049 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 17416 0 0 0 43814 87 0 0 25 0 1 0 1855203891 59277312 13229 4294967295 134512640 135094434 3221224432 3221223024 134557339 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 14472 13229 145 145 0 14327 0 [pid=3270] vsize: 57888 Current children cumulated CPU time (s) 439.01 Current children cumulated vsize (Kb) 60012 [startup+450.05 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 17638 0 0 0 44810 89 0 0 25 0 1 0 1855203891 60178432 13451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 14692 13451 145 145 0 14547 0 [pid=3270] vsize: 58768 Current children cumulated CPU time (s) 448.99 Current children cumulated vsize (Kb) 60892 [startup+460.051 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 17963 0 0 0 45804 91 0 0 25 0 1 0 1855203891 61501440 13776 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 15015 13776 145 145 0 14870 0 [pid=3270] vsize: 60060 Current children cumulated CPU time (s) 458.95 Current children cumulated vsize (Kb) 62184 [startup+470.052 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 18247 0 0 0 46800 93 0 0 25 0 1 0 1855203891 62660608 14060 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 15298 14060 145 145 0 15153 0 [pid=3270] vsize: 61192 Current children cumulated CPU time (s) 468.93 Current children cumulated vsize (Kb) 63316 [startup+480.052 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 18477 0 0 0 47796 95 0 0 25 0 1 0 1855203891 63598592 14290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 15527 14290 145 145 0 15382 0 [pid=3270] vsize: 62108 Current children cumulated CPU time (s) 478.91 Current children cumulated vsize (Kb) 64232 [startup+490.053 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 18533 0 0 0 48795 95 0 0 25 0 1 0 1855203891 63823872 14346 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 15582 14346 145 145 0 15437 0 [pid=3270] vsize: 62328 Current children cumulated CPU time (s) 488.9 Current children cumulated vsize (Kb) 64452 [startup+500.055 s] Raw data (loadavg): 1.00 1.00 0.82 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 18708 0 0 0 49791 97 0 0 25 0 1 0 1855203891 64536576 14521 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 15756 14521 145 145 0 15611 0 [pid=3270] vsize: 63024 Current children cumulated CPU time (s) 498.88 Current children cumulated vsize (Kb) 65148 [startup+510.056 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 18960 0 0 0 50787 99 0 0 25 0 1 0 1855203891 65564672 14773 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16007 14773 145 145 0 15862 0 [pid=3270] vsize: 64028 Current children cumulated CPU time (s) 508.86 Current children cumulated vsize (Kb) 66152 [startup+520.057 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19100 0 0 0 51785 100 0 0 25 0 1 0 1855203891 66134016 14913 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16146 14913 145 145 0 16001 0 [pid=3270] vsize: 64584 Current children cumulated CPU time (s) 518.85 Current children cumulated vsize (Kb) 66708 [startup+530.057 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19223 0 0 0 52784 100 0 0 25 0 1 0 1855203891 67006464 15036 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16359 15036 145 145 0 16214 0 [pid=3270] vsize: 65436 Current children cumulated CPU time (s) 528.84 Current children cumulated vsize (Kb) 67560 [startup+540.058 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19290 0 0 0 53783 101 0 0 25 0 1 0 1855203891 67289088 15103 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 16428 15103 145 145 0 16283 0 [pid=3270] vsize: 65712 Current children cumulated CPU time (s) 538.84 Current children cumulated vsize (Kb) 67836 [startup+550.06 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19409 0 0 0 54780 102 0 0 25 0 1 0 1855203891 67768320 15222 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 16545 15222 145 145 0 16400 0 [pid=3270] vsize: 66180 Current children cumulated CPU time (s) 548.82 Current children cumulated vsize (Kb) 68304 [startup+560.061 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19560 0 0 0 55778 103 0 0 25 0 1 0 1855203891 68378624 15373 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16694 15373 145 145 0 16549 0 [pid=3270] vsize: 66776 Current children cumulated CPU time (s) 558.81 Current children cumulated vsize (Kb) 68900 [startup+570.062 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19633 0 0 0 56777 103 0 0 25 0 1 0 1855203891 68673536 15446 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16766 15446 145 145 0 16621 0 [pid=3270] vsize: 67064 Current children cumulated CPU time (s) 568.8 Current children cumulated vsize (Kb) 69188 [startup+580.062 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19675 0 0 0 57777 104 0 0 25 0 1 0 1855203891 68845568 15488 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16808 15488 145 145 0 16663 0 [pid=3270] vsize: 67232 Current children cumulated CPU time (s) 578.81 Current children cumulated vsize (Kb) 69356 [startup+590.063 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19714 0 0 0 58777 104 0 0 25 0 1 0 1855203891 69005312 15527 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16847 15527 145 145 0 16702 0 [pid=3270] vsize: 67388 Current children cumulated CPU time (s) 588.81 Current children cumulated vsize (Kb) 69512 [startup+600.063 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19813 0 0 0 59775 104 0 0 25 0 1 0 1855203891 69410816 15626 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 16946 15626 145 145 0 16801 0 [pid=3270] vsize: 67784 Current children cumulated CPU time (s) 598.79 Current children cumulated vsize (Kb) 69908 [startup+610.064 s] Raw data (loadavg): 1.00 1.00 0.83 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 19932 0 0 0 60774 106 0 0 25 0 1 0 1855203891 69894144 15745 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17064 15745 145 145 0 16919 0 [pid=3270] vsize: 68256 Current children cumulated CPU time (s) 608.8 Current children cumulated vsize (Kb) 70380 [startup+620.064 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20025 0 0 0 61773 106 0 0 25 0 1 0 1855203891 70275072 15838 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17157 15838 145 145 0 17012 0 [pid=3270] vsize: 68628 Current children cumulated CPU time (s) 618.79 Current children cumulated vsize (Kb) 70752 [startup+630.065 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20130 0 0 0 62772 106 0 0 25 0 1 0 1855203891 70701056 15943 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17261 15943 145 145 0 17116 0 [pid=3270] vsize: 69044 Current children cumulated CPU time (s) 628.78 Current children cumulated vsize (Kb) 71168 [startup+640.066 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20237 0 0 0 63771 107 0 0 25 0 1 0 1855203891 71135232 16050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17367 16050 145 145 0 17222 0 [pid=3270] vsize: 69468 Current children cumulated CPU time (s) 638.78 Current children cumulated vsize (Kb) 71592 [startup+650.067 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20352 0 0 0 64769 107 0 0 25 0 1 0 1855203891 71606272 16165 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17482 16165 145 145 0 17337 0 [pid=3270] vsize: 69928 Current children cumulated CPU time (s) 648.76 Current children cumulated vsize (Kb) 72052 [startup+660.068 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20454 0 0 0 65767 108 0 0 25 0 1 0 1855203891 72019968 16267 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17583 16267 145 145 0 17438 0 [pid=3270] vsize: 70332 Current children cumulated CPU time (s) 658.75 Current children cumulated vsize (Kb) 72456 [startup+670.067 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20552 0 0 0 66766 109 0 0 25 0 1 0 1855203891 72421376 16365 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17681 16365 145 145 0 17536 0 [pid=3270] vsize: 70724 Current children cumulated CPU time (s) 668.75 Current children cumulated vsize (Kb) 72848 [startup+680.069 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20668 0 0 0 67765 110 0 0 25 0 1 0 1855203891 72892416 16481 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17796 16481 145 145 0 17651 0 [pid=3270] vsize: 71184 Current children cumulated CPU time (s) 678.75 Current children cumulated vsize (Kb) 73308 [startup+690.07 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20720 0 0 0 68764 110 0 0 25 0 1 0 1855203891 73105408 16533 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17848 16533 145 145 0 17703 0 [pid=3270] vsize: 71392 Current children cumulated CPU time (s) 688.74 Current children cumulated vsize (Kb) 73516 [startup+700.07 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20772 0 0 0 69764 110 0 0 25 0 1 0 1855203891 73318400 16585 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17900 16585 145 145 0 17755 0 [pid=3270] vsize: 71600 Current children cumulated CPU time (s) 698.74 Current children cumulated vsize (Kb) 73724 [startup+710.071 s] Raw data (loadavg): 1.00 1.00 0.84 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20844 0 0 0 70763 111 0 0 25 0 1 0 1855203891 73605120 16657 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 17970 16657 145 145 0 17825 0 [pid=3270] vsize: 71880 Current children cumulated CPU time (s) 708.74 Current children cumulated vsize (Kb) 74004 [startup+720.071 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 20967 0 0 0 71761 111 0 0 25 0 1 0 1855203891 74104832 16780 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18092 16780 145 145 0 17947 0 [pid=3270] vsize: 72368 Current children cumulated CPU time (s) 718.72 Current children cumulated vsize (Kb) 74492 [startup+730.072 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21071 0 0 0 72760 112 0 0 25 0 1 0 1855203891 74526720 16884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18195 16884 145 145 0 18050 0 [pid=3270] vsize: 72780 Current children cumulated CPU time (s) 728.72 Current children cumulated vsize (Kb) 74904 [startup+740.073 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21198 0 0 0 73758 113 0 0 25 0 1 0 1855203891 75042816 17011 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18321 17011 145 145 0 18176 0 [pid=3270] vsize: 73284 Current children cumulated CPU time (s) 738.71 Current children cumulated vsize (Kb) 75408 [startup+750.074 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21268 0 0 0 74756 114 0 0 25 0 1 0 1855203891 75333632 17081 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 18392 17081 145 145 0 18247 0 [pid=3270] vsize: 73568 Current children cumulated CPU time (s) 748.7 Current children cumulated vsize (Kb) 75692 [startup+760.076 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21340 0 0 0 75755 115 0 0 25 0 1 0 1855203891 75636736 17153 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 18466 17153 145 145 0 18321 0 [pid=3270] vsize: 73864 Current children cumulated CPU time (s) 758.7 Current children cumulated vsize (Kb) 75988 [startup+770.076 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21462 0 0 0 76753 116 0 0 25 0 1 0 1855203891 76136448 17275 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18588 17275 145 145 0 18443 0 [pid=3270] vsize: 74352 Current children cumulated CPU time (s) 768.69 Current children cumulated vsize (Kb) 76476 [startup+780.078 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21530 0 0 0 77751 116 0 0 25 0 1 0 1855203891 76423168 17343 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 18658 17343 145 145 0 18513 0 [pid=3270] vsize: 74632 Current children cumulated CPU time (s) 778.67 Current children cumulated vsize (Kb) 76756 [startup+790.079 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21569 0 0 0 78751 117 0 0 25 0 1 0 1855203891 76582912 17382 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 18697 17382 145 145 0 18552 0 [pid=3270] vsize: 74788 Current children cumulated CPU time (s) 788.68 Current children cumulated vsize (Kb) 76912 [startup+800.08 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21615 0 0 0 79749 117 0 0 25 0 1 0 1855203891 76771328 17428 4294967295 134512640 135094434 3221224432 3221223072 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18743 17428 145 145 0 18598 0 [pid=3270] vsize: 74972 Current children cumulated CPU time (s) 798.66 Current children cumulated vsize (Kb) 77096 [startup+810.08 s] Raw data (loadavg): 1.00 1.00 0.85 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21644 0 0 0 80749 117 0 0 25 0 1 0 1855203891 76886016 17457 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18771 17457 145 145 0 18626 0 [pid=3270] vsize: 75084 Current children cumulated CPU time (s) 808.66 Current children cumulated vsize (Kb) 77208 [startup+820.08 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21675 0 0 0 81749 118 0 0 25 0 1 0 1855203891 77017088 17488 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18803 17488 145 145 0 18658 0 [pid=3270] vsize: 75212 Current children cumulated CPU time (s) 818.67 Current children cumulated vsize (Kb) 77336 [startup+830.082 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21689 0 0 0 82749 118 0 0 25 0 1 0 1855203891 77070336 17502 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18816 17502 145 145 0 18671 0 [pid=3270] vsize: 75264 Current children cumulated CPU time (s) 828.67 Current children cumulated vsize (Kb) 77388 [startup+840.083 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21703 0 0 0 83749 118 0 0 25 0 1 0 1855203891 77123584 17516 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18829 17516 145 145 0 18684 0 [pid=3270] vsize: 75316 Current children cumulated CPU time (s) 838.67 Current children cumulated vsize (Kb) 77440 [startup+850.083 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21731 0 0 0 84748 118 0 0 25 0 1 0 1855203891 77238272 17544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18857 17544 145 145 0 18712 0 [pid=3270] vsize: 75428 Current children cumulated CPU time (s) 848.66 Current children cumulated vsize (Kb) 77552 [startup+860.083 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21756 0 0 0 85748 118 0 0 25 0 1 0 1855203891 77336576 17569 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18881 17569 145 145 0 18736 0 [pid=3270] vsize: 75524 Current children cumulated CPU time (s) 858.66 Current children cumulated vsize (Kb) 77648 [startup+870.084 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21774 0 0 0 86748 118 0 0 25 0 1 0 1855203891 77410304 17587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18899 17587 145 145 0 18754 0 [pid=3270] vsize: 75596 Current children cumulated CPU time (s) 868.66 Current children cumulated vsize (Kb) 77720 [startup+880.085 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21794 0 0 0 87748 118 0 0 25 0 1 0 1855203891 77492224 17607 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18919 17607 145 145 0 18774 0 [pid=3270] vsize: 75676 Current children cumulated CPU time (s) 878.66 Current children cumulated vsize (Kb) 77800 [startup+890.086 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21821 0 0 0 88748 118 0 0 25 0 1 0 1855203891 77606912 17634 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18947 17634 145 145 0 18802 0 [pid=3270] vsize: 75788 Current children cumulated CPU time (s) 888.66 Current children cumulated vsize (Kb) 77912 [startup+900.087 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21854 0 0 0 89748 118 0 0 25 0 1 0 1855203891 77737984 17667 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18979 17667 145 145 0 18834 0 [pid=3270] vsize: 75916 Current children cumulated CPU time (s) 898.66 Current children cumulated vsize (Kb) 78040 [startup+910.087 s] Raw data (loadavg): 1.00 1.00 0.86 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21871 0 0 0 90748 118 0 0 25 0 1 0 1855203891 77807616 17684 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 18996 17684 145 145 0 18851 0 [pid=3270] vsize: 75984 Current children cumulated CPU time (s) 908.66 Current children cumulated vsize (Kb) 78108 [startup+920.088 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21891 0 0 0 91747 118 0 0 25 0 1 0 1855203891 77889536 17704 4294967295 134512640 135094434 3221224432 3221223104 134555241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19016 17704 145 145 0 18871 0 [pid=3270] vsize: 76064 Current children cumulated CPU time (s) 918.65 Current children cumulated vsize (Kb) 78188 [startup+930.09 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21934 0 0 0 92747 119 0 0 25 0 1 0 1855203891 78061568 17747 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19058 17747 145 145 0 18913 0 [pid=3270] vsize: 76232 Current children cumulated CPU time (s) 928.66 Current children cumulated vsize (Kb) 78356 [startup+940.091 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21966 0 0 0 93747 119 0 0 25 0 1 0 1855203891 78196736 17779 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19091 17779 145 145 0 18946 0 [pid=3270] vsize: 76364 Current children cumulated CPU time (s) 938.66 Current children cumulated vsize (Kb) 78488 [startup+950.091 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 21993 0 0 0 94746 119 0 0 25 0 1 0 1855203891 78307328 17806 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19118 17806 145 145 0 18973 0 [pid=3270] vsize: 76472 Current children cumulated CPU time (s) 948.65 Current children cumulated vsize (Kb) 78596 [startup+960.092 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22028 0 0 0 95746 119 0 0 25 0 1 0 1855203891 78446592 17841 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19152 17841 145 145 0 19007 0 [pid=3270] vsize: 76608 Current children cumulated CPU time (s) 958.65 Current children cumulated vsize (Kb) 78732 [startup+970.092 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22052 0 0 0 96746 119 0 0 25 0 1 0 1855203891 78544896 17865 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19176 17865 145 145 0 19031 0 [pid=3270] vsize: 76704 Current children cumulated CPU time (s) 968.65 Current children cumulated vsize (Kb) 78828 [startup+980.094 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22079 0 0 0 97746 120 0 0 25 0 1 0 1855203891 78651392 17892 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19202 17892 145 145 0 19057 0 [pid=3270] vsize: 76808 Current children cumulated CPU time (s) 978.66 Current children cumulated vsize (Kb) 78932 [startup+990.095 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22105 0 0 0 98746 120 0 0 25 0 1 0 1855203891 78757888 17918 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19228 17918 145 145 0 19083 0 [pid=3270] vsize: 76912 Current children cumulated CPU time (s) 988.66 Current children cumulated vsize (Kb) 79036 [startup+1000.09 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22122 0 0 0 99746 120 0 0 25 0 1 0 1855203891 78823424 17935 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19244 17935 145 145 0 19099 0 [pid=3270] vsize: 76976 Current children cumulated CPU time (s) 998.66 Current children cumulated vsize (Kb) 79100 [startup+1010.1 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22141 0 0 0 100746 120 0 0 25 0 1 0 1855203891 78905344 17954 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19264 17954 145 145 0 19119 0 [pid=3270] vsize: 77056 Current children cumulated CPU time (s) 1008.66 Current children cumulated vsize (Kb) 79180 [startup+1020.1 s] Raw data (loadavg): 1.00 1.00 0.87 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22193 0 0 0 101745 120 0 0 25 0 1 0 1855203891 79110144 18006 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19314 18006 145 145 0 19169 0 [pid=3270] vsize: 77256 Current children cumulated CPU time (s) 1018.65 Current children cumulated vsize (Kb) 79380 [startup+1030.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22313 0 0 0 102744 121 0 0 25 0 1 0 1855203891 79601664 18126 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19434 18126 145 145 0 19289 0 [pid=3270] vsize: 77736 Current children cumulated CPU time (s) 1028.65 Current children cumulated vsize (Kb) 79860 [startup+1040.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22419 0 0 0 103744 122 0 0 25 0 1 0 1855203891 80039936 18232 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19541 18232 145 145 0 19396 0 [pid=3270] vsize: 78164 Current children cumulated CPU time (s) 1038.66 Current children cumulated vsize (Kb) 80288 [startup+1050.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22501 0 0 0 104743 122 0 0 25 0 1 0 1855203891 80367616 18314 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19621 18314 145 145 0 19476 0 [pid=3270] vsize: 78484 Current children cumulated CPU time (s) 1048.65 Current children cumulated vsize (Kb) 80608 [startup+1060.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22591 0 0 0 105742 123 0 0 25 0 1 0 1855203891 80740352 18404 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19712 18404 145 145 0 19567 0 [pid=3270] vsize: 78848 Current children cumulated CPU time (s) 1058.65 Current children cumulated vsize (Kb) 80972 [startup+1070.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22681 0 0 0 106741 123 0 0 25 0 1 0 1855203891 81113088 18494 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19803 18494 145 145 0 19658 0 [pid=3270] vsize: 79212 Current children cumulated CPU time (s) 1068.64 Current children cumulated vsize (Kb) 81336 [startup+1080.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22746 0 0 0 107741 124 0 0 25 0 1 0 1855203891 81383424 18559 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19869 18559 145 145 0 19724 0 [pid=3270] vsize: 79476 Current children cumulated CPU time (s) 1078.65 Current children cumulated vsize (Kb) 81600 [startup+1090.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22839 0 0 0 108740 124 0 0 25 0 1 0 1855203891 81764352 18652 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 19962 18652 145 145 0 19817 0 [pid=3270] vsize: 79848 Current children cumulated CPU time (s) 1088.64 Current children cumulated vsize (Kb) 81972 [startup+1100.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22906 0 0 0 109740 124 0 0 25 0 1 0 1855203891 82030592 18719 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20027 18719 145 145 0 19882 0 [pid=3270] vsize: 80108 Current children cumulated CPU time (s) 1098.64 Current children cumulated vsize (Kb) 82232 [startup+1110.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 22974 0 0 0 110739 124 0 0 25 0 1 0 1855203891 82309120 18787 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20095 18787 145 145 0 19950 0 [pid=3270] vsize: 80380 Current children cumulated CPU time (s) 1108.63 Current children cumulated vsize (Kb) 82504 [startup+1120.1 s] Raw data (loadavg): 1.00 1.00 0.88 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 111737 125 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1118.62 Current children cumulated vsize (Kb) 82748 [startup+1130.1 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 112736 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1128.62 Current children cumulated vsize (Kb) 82748 [startup+1140.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 113736 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1138.62 Current children cumulated vsize (Kb) 82748 [startup+1150.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 114736 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1148.62 Current children cumulated vsize (Kb) 82748 [startup+1160.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 115736 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1158.62 Current children cumulated vsize (Kb) 82748 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 116736 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1168.62 Current children cumulated vsize (Kb) 82748 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 117737 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1178.63 Current children cumulated vsize (Kb) 82748 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 118737 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1188.63 Current children cumulated vsize (Kb) 82748 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 119737 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1198.63 Current children cumulated vsize (Kb) 82748 [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 120737 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1208.63 Current children cumulated vsize (Kb) 82748 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.89 2/57 3270 Raw data (/proc/3266/stat): 3266 (minisat+_script) S 3265 3266 5245 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1855203886 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/3266/statm): 531 226 485 147 0 384 0 [pid=3266] vsize: 2124 Raw data (/proc/3270/stat): 3270 (minisat+_64-bit) R 3266 3266 5245 0 -1 0 23099 0 0 0 120737 126 0 0 25 0 1 0 1855203891 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/3270/statm): 20156 18848 145 145 0 20011 0 [pid=3270] vsize: 80624 Current children cumulated CPU time (s) 1208.63 Current children cumulated vsize (Kb) 82748 Sending SIGTERM to -3266 Sleeping 2 seconds One traced child (pid=3266) ended because it received signal 15 (SIGTERM) One traced child (pid=3270) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.15 CPU time (s): 1208.68 CPU user time (s): 1207.38 CPU system time (s): 1.3058 CPU usage (%): 99.8784 Max. virtual memory (cumulated for all children) (Kb): 82748
ERROR: no interpretation found !