Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mod008.opb |
MD5SUM | 581d778a36086562107993896110e0a2 |
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.05 |
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 wulflinc7 THE 2005-09-20 04:43:27 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3402 boxname=wulflinc7 idbench=1058 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 581d778a36086562107993896110e0a2 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb IDLAUNCH: 3402 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 906384 kB Buffers: 8508 kB Cached: 94584 kB SwapCached: 744 kB Active: 26332 kB Inactive: 79412 kB HighTotal: 131008 kB HighFree: 32228 kB LowTotal: 903652 kB LowFree: 874156 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5668 kB Slab: 16644 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:03:37 (client local time) WITH STATUS 10 IN 1208.75 SECONDS stats: 3402 7 1208.75 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/10556/stat): 10556 (minisat+_script) R 10555 10556 15400 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797544617 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10556/statm): 174 3 169 147 0 27 0 [pid=10556] 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=10557 New process pid=10558 New process pid=10559 One traced child (pid=10558) exited with status: 0 execve syscall for /bin/sed executable 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=10559) exited with status: 0 One traced child (pid=10557) exited with status: 0 New process pid=10560 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-mod008.opb [startup+10.0036 s] Raw data (loadavg): 0.87 0.94 0.90 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 4707 0 0 0 971 14 0 0 25 0 1 0 1797544622 5906432 1286 4294967295 134512640 135094434 3221224432 3221221280 134676552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 1442 1286 145 145 0 1297 0 [pid=10560] vsize: 5768 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 7892 [startup+20.0043 s] Raw data (loadavg): 0.89 0.94 0.90 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9625 0 0 0 1932 32 0 0 25 0 1 0 1797544622 28651520 5736 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 6995 5736 145 145 0 6850 0 [pid=10560] vsize: 27980 Current children cumulated CPU time (s) 19.64 Current children cumulated vsize (Kb) 30104 [startup+30.0059 s] Raw data (loadavg): 0.91 0.94 0.90 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9680 0 0 0 2930 33 0 0 25 0 1 0 1797544622 28823552 5791 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7037 5791 145 145 0 6892 0 [pid=10560] vsize: 28148 Current children cumulated CPU time (s) 29.63 Current children cumulated vsize (Kb) 30272 [startup+40.0065 s] Raw data (loadavg): 0.92 0.94 0.90 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9815 0 0 0 3927 34 0 0 25 0 1 0 1797544622 29360128 5926 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7168 5926 145 145 0 7023 0 [pid=10560] vsize: 28672 Current children cumulated CPU time (s) 39.61 Current children cumulated vsize (Kb) 30796 [startup+50.0081 s] Raw data (loadavg): 0.93 0.94 0.90 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 9969 0 0 0 4924 35 0 0 25 0 1 0 1797544622 29970432 6080 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7317 6080 145 145 0 7172 0 [pid=10560] vsize: 29268 Current children cumulated CPU time (s) 49.59 Current children cumulated vsize (Kb) 31392 [startup+60.0088 s] Raw data (loadavg): 0.94 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10242 0 0 0 5921 37 0 0 25 0 1 0 1797544622 30896128 6311 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7543 6311 145 145 0 7398 0 [pid=10560] vsize: 30172 Current children cumulated CPU time (s) 59.58 Current children cumulated vsize (Kb) 32296 [startup+70.0094 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10263 0 0 0 6921 38 0 0 25 0 1 0 1797544622 30978048 6332 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7563 6332 145 145 0 7418 0 [pid=10560] vsize: 30252 Current children cumulated CPU time (s) 69.59 Current children cumulated vsize (Kb) 32376 [startup+80.011 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10309 0 0 0 7920 38 0 0 25 0 1 0 1797544622 31227904 6378 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7624 6378 145 145 0 7479 0 [pid=10560] vsize: 30496 Current children cumulated CPU time (s) 79.58 Current children cumulated vsize (Kb) 32620 [startup+90.0117 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10424 0 0 0 8918 39 0 0 25 0 1 0 1797544622 31424512 6428 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7672 6428 145 145 0 7527 0 [pid=10560] vsize: 30688 Current children cumulated CPU time (s) 89.57 Current children cumulated vsize (Kb) 32812 [startup+100.012 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10494 0 0 0 9917 40 0 0 25 0 1 0 1797544622 31715328 6498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 7743 6498 145 145 0 7598 0 [pid=10560] vsize: 30972 Current children cumulated CPU time (s) 99.57 Current children cumulated vsize (Kb) 33096 [startup+110.014 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10584 0 0 0 10915 41 0 0 25 0 1 0 1797544622 32079872 6588 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 7832 6588 145 145 0 7687 0 [pid=10560] vsize: 31328 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 33452 [startup+120.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 10849 0 0 0 11912 43 0 0 25 0 1 0 1797544622 32632832 6726 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 7967 6726 145 145 0 7822 0 [pid=10560] vsize: 31868 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 33992 [startup+130.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11014 0 0 0 12909 44 0 0 25 0 1 0 1797544622 33361920 6891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8145 6891 145 145 0 8000 0 [pid=10560] vsize: 32580 Current children cumulated CPU time (s) 129.53 Current children cumulated vsize (Kb) 34704 [startup+140.016 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11236 0 0 0 13906 46 0 0 25 0 1 0 1797544622 34000896 7049 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8301 7049 145 145 0 8156 0 [pid=10560] vsize: 33204 Current children cumulated CPU time (s) 139.52 Current children cumulated vsize (Kb) 35328 [startup+150.016 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11292 0 0 0 14905 47 0 0 25 0 1 0 1797544622 34226176 7105 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8356 7105 145 145 0 8211 0 [pid=10560] vsize: 33424 Current children cumulated CPU time (s) 149.52 Current children cumulated vsize (Kb) 35548 [startup+160.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11399 0 0 0 15903 47 0 0 25 0 1 0 1797544622 34660352 7212 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8462 7212 145 145 0 8317 0 [pid=10560] vsize: 33848 Current children cumulated CPU time (s) 159.5 Current children cumulated vsize (Kb) 35972 [startup+170.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11463 0 0 0 16902 48 0 0 25 0 1 0 1797544622 34922496 7276 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8526 7276 145 145 0 8381 0 [pid=10560] vsize: 34104 Current children cumulated CPU time (s) 169.5 Current children cumulated vsize (Kb) 36228 [startup+180.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11514 0 0 0 17902 48 0 0 25 0 1 0 1797544622 35090432 7327 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 8567 7327 145 145 0 8422 0 [pid=10560] vsize: 34268 Current children cumulated CPU time (s) 179.5 Current children cumulated vsize (Kb) 36392 [startup+190.018 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11685 0 0 0 18900 49 0 0 25 0 1 0 1797544622 35786752 7498 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 8737 7498 145 145 0 8592 0 [pid=10560] vsize: 34948 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 37072 [startup+200.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 11888 0 0 0 19897 51 0 0 25 0 1 0 1797544622 36614144 7701 4294967295 134512640 135094434 3221224432 3221223024 134557044 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 8939 7701 145 145 0 8794 0 [pid=10560] vsize: 35756 Current children cumulated CPU time (s) 199.48 Current children cumulated vsize (Kb) 37880 [startup+210.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12190 0 0 0 20892 53 0 0 25 0 1 0 1797544622 37847040 8003 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 9240 8003 145 145 0 9095 0 [pid=10560] vsize: 36960 Current children cumulated CPU time (s) 209.45 Current children cumulated vsize (Kb) 39084 [startup+220.021 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12679 0 0 0 21885 56 0 0 25 0 1 0 1797544622 39845888 8492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 9728 8492 145 145 0 9583 0 [pid=10560] vsize: 38912 Current children cumulated CPU time (s) 219.41 Current children cumulated vsize (Kb) 41036 [startup+230.022 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 12869 0 0 0 22882 57 0 0 25 0 1 0 1797544622 40620032 8682 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/10560/statm): 9917 8682 145 145 0 9772 0 [pid=10560] vsize: 39668 Current children cumulated CPU time (s) 229.39 Current children cumulated vsize (Kb) 41792 [startup+240.023 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13238 0 0 0 23874 60 0 0 25 0 1 0 1797544622 42127360 9051 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 10285 9051 145 145 0 10140 0 [pid=10560] vsize: 41140 Current children cumulated CPU time (s) 239.34 Current children cumulated vsize (Kb) 43264 [startup+250.024 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13391 0 0 0 24873 61 0 0 25 0 1 0 1797544622 42881024 9204 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 10469 9204 145 145 0 10324 0 [pid=10560] vsize: 41876 Current children cumulated CPU time (s) 249.34 Current children cumulated vsize (Kb) 44000 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13600 0 0 0 25869 62 0 0 25 0 1 0 1797544622 43732992 9413 4294967295 134512640 135094434 3221224432 3221223128 134784927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 10677 9413 145 145 0 10532 0 [pid=10560] vsize: 42708 Current children cumulated CPU time (s) 259.31 Current children cumulated vsize (Kb) 44832 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 13903 0 0 0 26865 64 0 0 25 0 1 0 1797544622 44969984 9716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 10979 9716 145 145 0 10834 0 [pid=10560] vsize: 43916 Current children cumulated CPU time (s) 269.29 Current children cumulated vsize (Kb) 46040 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14134 0 0 0 27863 66 0 0 25 0 1 0 1797544622 45912064 9947 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 11209 9947 145 145 0 11064 0 [pid=10560] vsize: 44836 Current children cumulated CPU time (s) 279.29 Current children cumulated vsize (Kb) 46960 [startup+290.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14427 0 0 0 28859 68 0 0 25 0 1 0 1797544622 47108096 10240 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 11501 10240 145 145 0 11356 0 [pid=10560] vsize: 46004 Current children cumulated CPU time (s) 289.27 Current children cumulated vsize (Kb) 48128 [startup+300.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14585 0 0 0 29857 68 0 0 25 0 1 0 1797544622 47755264 10398 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 11659 10398 145 145 0 11514 0 [pid=10560] vsize: 46636 Current children cumulated CPU time (s) 299.25 Current children cumulated vsize (Kb) 48760 [startup+310.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 14880 0 0 0 30853 70 0 0 25 0 1 0 1797544622 48951296 10693 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 11951 10693 145 145 0 11806 0 [pid=10560] vsize: 47804 Current children cumulated CPU time (s) 309.23 Current children cumulated vsize (Kb) 49928 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15085 0 0 0 31851 71 0 0 25 0 1 0 1797544622 49790976 10898 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 12156 10898 145 145 0 12011 0 [pid=10560] vsize: 48624 Current children cumulated CPU time (s) 319.22 Current children cumulated vsize (Kb) 50748 [startup+330.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15287 0 0 0 32847 72 0 0 25 0 1 0 1797544622 50610176 11100 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 12356 11100 145 145 0 12211 0 [pid=10560] vsize: 49424 Current children cumulated CPU time (s) 329.19 Current children cumulated vsize (Kb) 51548 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15499 0 0 0 33845 73 0 0 25 0 1 0 1797544622 51474432 11312 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 12567 11312 145 145 0 12422 0 [pid=10560] vsize: 50268 Current children cumulated CPU time (s) 339.18 Current children cumulated vsize (Kb) 52392 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15746 0 0 0 34840 75 0 0 25 0 1 0 1797544622 52477952 11559 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 12812 11559 145 145 0 12667 0 [pid=10560] vsize: 51248 Current children cumulated CPU time (s) 349.15 Current children cumulated vsize (Kb) 53372 [startup+360.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 15900 0 0 0 35836 77 0 0 25 0 1 0 1797544622 53104640 11713 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 12965 11713 145 145 0 12820 0 [pid=10560] vsize: 51860 Current children cumulated CPU time (s) 359.13 Current children cumulated vsize (Kb) 53984 [startup+370.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16107 0 0 0 36833 79 0 0 25 0 1 0 1797544622 53948416 11920 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 13171 11920 145 145 0 13026 0 [pid=10560] vsize: 52684 Current children cumulated CPU time (s) 369.12 Current children cumulated vsize (Kb) 54808 [startup+380.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16320 0 0 0 37831 80 0 0 25 0 1 0 1797544622 54816768 12133 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 13383 12133 145 145 0 13238 0 [pid=10560] vsize: 53532 Current children cumulated CPU time (s) 379.11 Current children cumulated vsize (Kb) 55656 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16474 0 0 0 38829 81 0 0 25 0 1 0 1797544622 55447552 12287 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 13537 12287 145 145 0 13392 0 [pid=10560] vsize: 54148 Current children cumulated CPU time (s) 389.1 Current children cumulated vsize (Kb) 56272 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16720 0 0 0 39826 83 0 0 25 0 1 0 1797544622 56446976 12533 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 13781 12533 145 145 0 13636 0 [pid=10560] vsize: 55124 Current children cumulated CPU time (s) 399.09 Current children cumulated vsize (Kb) 57248 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 16962 0 0 0 40821 85 0 0 25 0 1 0 1797544622 57434112 12775 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 14022 12775 145 145 0 13877 0 [pid=10560] vsize: 56088 Current children cumulated CPU time (s) 409.06 Current children cumulated vsize (Kb) 58212 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17153 0 0 0 41818 86 0 0 25 0 1 0 1797544622 58208256 12966 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 14211 12966 145 145 0 14066 0 [pid=10560] vsize: 56844 Current children cumulated CPU time (s) 419.04 Current children cumulated vsize (Kb) 58968 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) T 10556 10556 15400 0 -1 0 17195 0 0 0 42818 86 0 0 25 0 1 0 1797544622 58376192 13008 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/10560/statm): 14252 13008 145 145 0 14107 0 [pid=10560] vsize: 57008 Current children cumulated CPU time (s) 429.04 Current children cumulated vsize (Kb) 59132 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17412 0 0 0 43815 87 0 0 25 0 1 0 1797544622 59260928 13225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 14468 13225 145 145 0 14323 0 [pid=10560] vsize: 57872 Current children cumulated CPU time (s) 439.02 Current children cumulated vsize (Kb) 59996 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17634 0 0 0 44810 89 0 0 25 0 1 0 1797544622 60162048 13447 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 14688 13447 145 145 0 14543 0 [pid=10560] vsize: 58752 Current children cumulated CPU time (s) 448.99 Current children cumulated vsize (Kb) 60876 [startup+460.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 17959 0 0 0 45806 90 0 0 25 0 1 0 1797544622 61485056 13772 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 15011 13772 145 145 0 14866 0 [pid=10560] vsize: 60044 Current children cumulated CPU time (s) 458.96 Current children cumulated vsize (Kb) 62168 [startup+470.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18242 0 0 0 46801 92 0 0 25 0 1 0 1797544622 62640128 14055 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 15293 14055 145 145 0 15148 0 [pid=10560] vsize: 61172 Current children cumulated CPU time (s) 468.93 Current children cumulated vsize (Kb) 63296 [startup+480.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18477 0 0 0 47797 94 0 0 25 0 1 0 1797544622 63598592 14290 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 15527 14290 145 145 0 15382 0 [pid=10560] vsize: 62108 Current children cumulated CPU time (s) 478.91 Current children cumulated vsize (Kb) 64232 [startup+490.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18532 0 0 0 48796 95 0 0 25 0 1 0 1797544622 63819776 14345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 15581 14345 145 145 0 15436 0 [pid=10560] vsize: 62324 Current children cumulated CPU time (s) 488.91 Current children cumulated vsize (Kb) 64448 [startup+500.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18708 0 0 0 49794 96 0 0 25 0 1 0 1797544622 64536576 14521 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 15756 14521 145 145 0 15611 0 [pid=10560] vsize: 63024 Current children cumulated CPU time (s) 498.9 Current children cumulated vsize (Kb) 65148 [startup+510.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 18958 0 0 0 50790 97 0 0 25 0 1 0 1797544622 65556480 14771 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16005 14771 145 145 0 15860 0 [pid=10560] vsize: 64020 Current children cumulated CPU time (s) 508.87 Current children cumulated vsize (Kb) 66144 [startup+520.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19096 0 0 0 51787 99 0 0 25 0 1 0 1797544622 66117632 14909 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16142 14909 145 145 0 15997 0 [pid=10560] vsize: 64568 Current children cumulated CPU time (s) 518.86 Current children cumulated vsize (Kb) 66692 [startup+530.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19223 0 0 0 52785 101 0 0 25 0 1 0 1797544622 67006464 15036 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16359 15036 145 145 0 16214 0 [pid=10560] vsize: 65436 Current children cumulated CPU time (s) 528.86 Current children cumulated vsize (Kb) 67560 [startup+540.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19290 0 0 0 53785 101 0 0 25 0 1 0 1797544622 67289088 15103 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16428 15103 145 145 0 16283 0 [pid=10560] vsize: 65712 Current children cumulated CPU time (s) 538.86 Current children cumulated vsize (Kb) 67836 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19407 0 0 0 54784 102 0 0 25 0 1 0 1797544622 67760128 15220 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16543 15220 145 145 0 16398 0 [pid=10560] vsize: 66172 Current children cumulated CPU time (s) 548.86 Current children cumulated vsize (Kb) 68296 [startup+560.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19560 0 0 0 55783 102 0 0 25 0 1 0 1797544622 68378624 15373 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16694 15373 145 145 0 16549 0 [pid=10560] vsize: 66776 Current children cumulated CPU time (s) 558.85 Current children cumulated vsize (Kb) 68900 [startup+570.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19633 0 0 0 56781 103 0 0 25 0 1 0 1797544622 68673536 15446 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16766 15446 145 145 0 16621 0 [pid=10560] vsize: 67064 Current children cumulated CPU time (s) 568.84 Current children cumulated vsize (Kb) 69188 [startup+580.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19675 0 0 0 57781 103 0 0 25 0 1 0 1797544622 68845568 15488 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16808 15488 145 145 0 16663 0 [pid=10560] vsize: 67232 Current children cumulated CPU time (s) 578.84 Current children cumulated vsize (Kb) 69356 [startup+590.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19713 0 0 0 58781 103 0 0 25 0 1 0 1797544622 69001216 15526 4294967295 134512640 135094434 3221224432 3221223024 134556823 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16846 15526 145 145 0 16701 0 [pid=10560] vsize: 67384 Current children cumulated CPU time (s) 588.84 Current children cumulated vsize (Kb) 69508 [startup+600.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19809 0 0 0 59780 104 0 0 25 0 1 0 1797544622 69394432 15622 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 16942 15622 145 145 0 16797 0 [pid=10560] vsize: 67768 Current children cumulated CPU time (s) 598.84 Current children cumulated vsize (Kb) 69892 [startup+610.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 19930 0 0 0 60778 104 0 0 25 0 1 0 1797544622 69885952 15743 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17062 15743 145 145 0 16917 0 [pid=10560] vsize: 68248 Current children cumulated CPU time (s) 608.82 Current children cumulated vsize (Kb) 70372 [startup+620.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20024 0 0 0 61777 105 0 0 25 0 1 0 1797544622 70275072 15837 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17157 15837 145 145 0 17012 0 [pid=10560] vsize: 68628 Current children cumulated CPU time (s) 618.82 Current children cumulated vsize (Kb) 70752 [startup+630.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20130 0 0 0 62776 105 0 0 25 0 1 0 1797544622 70701056 15943 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17261 15943 145 145 0 17116 0 [pid=10560] vsize: 69044 Current children cumulated CPU time (s) 628.81 Current children cumulated vsize (Kb) 71168 [startup+640.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20237 0 0 0 63774 106 0 0 25 0 1 0 1797544622 71135232 16050 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17367 16050 145 145 0 17222 0 [pid=10560] vsize: 69468 Current children cumulated CPU time (s) 638.8 Current children cumulated vsize (Kb) 71592 [startup+650.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20344 0 0 0 64773 107 0 0 25 0 1 0 1797544622 71581696 16157 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17476 16157 145 145 0 17331 0 [pid=10560] vsize: 69904 Current children cumulated CPU time (s) 648.8 Current children cumulated vsize (Kb) 72028 [startup+660.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20454 0 0 0 65771 107 0 0 25 0 1 0 1797544622 72019968 16267 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17583 16267 145 145 0 17438 0 [pid=10560] vsize: 70332 Current children cumulated CPU time (s) 658.78 Current children cumulated vsize (Kb) 72456 [startup+670.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20551 0 0 0 66770 108 0 0 25 0 1 0 1797544622 72417280 16364 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17680 16364 145 145 0 17535 0 [pid=10560] vsize: 70720 Current children cumulated CPU time (s) 668.78 Current children cumulated vsize (Kb) 72844 [startup+680.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20666 0 0 0 67768 109 0 0 25 0 1 0 1797544622 72884224 16479 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17794 16479 145 145 0 17649 0 [pid=10560] vsize: 71176 Current children cumulated CPU time (s) 678.77 Current children cumulated vsize (Kb) 73300 [startup+690.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20715 0 0 0 68768 109 0 0 25 0 1 0 1797544622 73084928 16528 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17843 16528 145 145 0 17698 0 [pid=10560] vsize: 71372 Current children cumulated CPU time (s) 688.77 Current children cumulated vsize (Kb) 73496 [startup+700.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20767 0 0 0 69768 109 0 0 25 0 1 0 1797544622 73297920 16580 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17895 16580 145 145 0 17750 0 [pid=10560] vsize: 71580 Current children cumulated CPU time (s) 698.77 Current children cumulated vsize (Kb) 73704 [startup+710.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20836 0 0 0 70767 109 0 0 25 0 1 0 1797544622 73572352 16649 4294967295 134512640 135094434 3221224432 3221223024 134557345 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 17962 16649 145 145 0 17817 0 [pid=10560] vsize: 71848 Current children cumulated CPU time (s) 708.76 Current children cumulated vsize (Kb) 73972 [startup+720.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 20957 0 0 0 71765 110 0 0 25 0 1 0 1797544622 74063872 16770 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18082 16770 145 145 0 17937 0 [pid=10560] vsize: 72328 Current children cumulated CPU time (s) 718.75 Current children cumulated vsize (Kb) 74452 [startup+730.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21063 0 0 0 72763 111 0 0 25 0 1 0 1797544622 74498048 16876 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18188 16876 145 145 0 18043 0 [pid=10560] vsize: 72752 Current children cumulated CPU time (s) 728.74 Current children cumulated vsize (Kb) 74876 [startup+740.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21187 0 0 0 73761 112 0 0 25 0 1 0 1797544622 75001856 17000 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18311 17000 145 145 0 18166 0 [pid=10560] vsize: 73244 Current children cumulated CPU time (s) 738.73 Current children cumulated vsize (Kb) 75368 [startup+750.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21267 0 0 0 74759 113 0 0 25 0 1 0 1797544622 75329536 17080 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18391 17080 145 145 0 18246 0 [pid=10560] vsize: 73564 Current children cumulated CPU time (s) 748.72 Current children cumulated vsize (Kb) 75688 [startup+760.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21333 0 0 0 75759 113 0 0 25 0 1 0 1797544622 75603968 17146 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18458 17146 145 145 0 18313 0 [pid=10560] vsize: 73832 Current children cumulated CPU time (s) 758.72 Current children cumulated vsize (Kb) 75956 [startup+770.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21459 0 0 0 76758 114 0 0 25 0 1 0 1797544622 76124160 17272 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18585 17272 145 145 0 18440 0 [pid=10560] vsize: 74340 Current children cumulated CPU time (s) 768.72 Current children cumulated vsize (Kb) 76464 [startup+780.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21528 0 0 0 77756 114 0 0 25 0 1 0 1797544622 76414976 17341 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18656 17341 145 145 0 18511 0 [pid=10560] vsize: 74624 Current children cumulated CPU time (s) 778.7 Current children cumulated vsize (Kb) 76748 [startup+790.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21569 0 0 0 78756 114 0 0 25 0 1 0 1797544622 76582912 17382 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18697 17382 145 145 0 18552 0 [pid=10560] vsize: 74788 Current children cumulated CPU time (s) 788.7 Current children cumulated vsize (Kb) 76912 [startup+800.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21615 0 0 0 79756 115 0 0 25 0 1 0 1797544622 76771328 17428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18743 17428 145 145 0 18598 0 [pid=10560] vsize: 74972 Current children cumulated CPU time (s) 798.71 Current children cumulated vsize (Kb) 77096 [startup+810.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21644 0 0 0 80755 115 0 0 25 0 1 0 1797544622 76886016 17457 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18771 17457 145 145 0 18626 0 [pid=10560] vsize: 75084 Current children cumulated CPU time (s) 808.7 Current children cumulated vsize (Kb) 77208 [startup+820.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21675 0 0 0 81755 115 0 0 25 0 1 0 1797544622 77017088 17488 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18803 17488 145 145 0 18658 0 [pid=10560] vsize: 75212 Current children cumulated CPU time (s) 818.7 Current children cumulated vsize (Kb) 77336 [startup+830.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21689 0 0 0 82755 115 0 0 25 0 1 0 1797544622 77070336 17502 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18816 17502 145 145 0 18671 0 [pid=10560] vsize: 75264 Current children cumulated CPU time (s) 828.7 Current children cumulated vsize (Kb) 77388 [startup+840.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21704 0 0 0 83755 115 0 0 25 0 1 0 1797544622 77127680 17517 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18830 17517 145 145 0 18685 0 [pid=10560] vsize: 75320 Current children cumulated CPU time (s) 838.7 Current children cumulated vsize (Kb) 77444 [startup+850.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21731 0 0 0 84755 116 0 0 25 0 1 0 1797544622 77238272 17544 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18857 17544 145 145 0 18712 0 [pid=10560] vsize: 75428 Current children cumulated CPU time (s) 848.71 Current children cumulated vsize (Kb) 77552 [startup+860.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21756 0 0 0 85755 116 0 0 25 0 1 0 1797544622 77336576 17569 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18881 17569 145 145 0 18736 0 [pid=10560] vsize: 75524 Current children cumulated CPU time (s) 858.71 Current children cumulated vsize (Kb) 77648 [startup+870.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21774 0 0 0 86755 116 0 0 25 0 1 0 1797544622 77410304 17587 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18899 17587 145 145 0 18754 0 [pid=10560] vsize: 75596 Current children cumulated CPU time (s) 868.71 Current children cumulated vsize (Kb) 77720 [startup+880.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21795 0 0 0 87756 116 0 0 25 0 1 0 1797544622 77496320 17608 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18920 17608 145 145 0 18775 0 [pid=10560] vsize: 75680 Current children cumulated CPU time (s) 878.72 Current children cumulated vsize (Kb) 77804 [startup+890.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21825 0 0 0 88755 116 0 0 25 0 1 0 1797544622 77623296 17638 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18951 17638 145 145 0 18806 0 [pid=10560] vsize: 75804 Current children cumulated CPU time (s) 888.71 Current children cumulated vsize (Kb) 77928 [startup+900.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21854 0 0 0 89755 116 0 0 25 0 1 0 1797544622 77737984 17667 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18979 17667 145 145 0 18834 0 [pid=10560] vsize: 75916 Current children cumulated CPU time (s) 898.71 Current children cumulated vsize (Kb) 78040 [startup+910.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21871 0 0 0 90755 116 0 0 25 0 1 0 1797544622 77807616 17684 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 18996 17684 145 145 0 18851 0 [pid=10560] vsize: 75984 Current children cumulated CPU time (s) 908.71 Current children cumulated vsize (Kb) 78108 [startup+920.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21893 0 0 0 91754 116 0 0 25 0 1 0 1797544622 77897728 17706 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19018 17706 145 145 0 18873 0 [pid=10560] vsize: 76072 Current children cumulated CPU time (s) 918.7 Current children cumulated vsize (Kb) 78196 [startup+930.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21938 0 0 0 92754 117 0 0 25 0 1 0 1797544622 78077952 17751 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19062 17751 145 145 0 18917 0 [pid=10560] vsize: 76248 Current children cumulated CPU time (s) 928.71 Current children cumulated vsize (Kb) 78372 [startup+940.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21970 0 0 0 93754 117 0 0 25 0 1 0 1797544622 78213120 17783 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19095 17783 145 145 0 18950 0 [pid=10560] vsize: 76380 Current children cumulated CPU time (s) 938.71 Current children cumulated vsize (Kb) 78504 [startup+950.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 21997 0 0 0 94753 117 0 0 25 0 1 0 1797544622 78323712 17810 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19122 17810 145 145 0 18977 0 [pid=10560] vsize: 76488 Current children cumulated CPU time (s) 948.7 Current children cumulated vsize (Kb) 78612 [startup+960.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22032 0 0 0 95753 117 0 0 25 0 1 0 1797544622 78462976 17845 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19156 17845 145 145 0 19011 0 [pid=10560] vsize: 76624 Current children cumulated CPU time (s) 958.7 Current children cumulated vsize (Kb) 78748 [startup+970.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22053 0 0 0 96753 117 0 0 25 0 1 0 1797544622 78548992 17866 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19177 17866 145 145 0 19032 0 [pid=10560] vsize: 76708 Current children cumulated CPU time (s) 968.7 Current children cumulated vsize (Kb) 78832 [startup+980.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22079 0 0 0 97753 117 0 0 25 0 1 0 1797544622 78651392 17892 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19202 17892 145 145 0 19057 0 [pid=10560] vsize: 76808 Current children cumulated CPU time (s) 978.7 Current children cumulated vsize (Kb) 78932 [startup+990.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22105 0 0 0 98753 118 0 0 25 0 1 0 1797544622 78757888 17918 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19228 17918 145 145 0 19083 0 [pid=10560] vsize: 76912 Current children cumulated CPU time (s) 988.71 Current children cumulated vsize (Kb) 79036 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22125 0 0 0 99753 118 0 0 25 0 1 0 1797544622 78839808 17938 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19248 17938 145 145 0 19103 0 [pid=10560] vsize: 76992 Current children cumulated CPU time (s) 998.71 Current children cumulated vsize (Kb) 79116 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22145 0 0 0 100753 118 0 0 25 0 1 0 1797544622 78921728 17958 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19268 17958 145 145 0 19123 0 [pid=10560] vsize: 77072 Current children cumulated CPU time (s) 1008.71 Current children cumulated vsize (Kb) 79196 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22207 0 0 0 101752 118 0 0 25 0 1 0 1797544622 79167488 18020 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19328 18020 145 145 0 19183 0 [pid=10560] vsize: 77312 Current children cumulated CPU time (s) 1018.7 Current children cumulated vsize (Kb) 79436 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22329 0 0 0 102751 120 0 0 25 0 1 0 1797544622 79667200 18142 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19450 18142 145 145 0 19305 0 [pid=10560] vsize: 77800 Current children cumulated CPU time (s) 1028.71 Current children cumulated vsize (Kb) 79924 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22426 0 0 0 103750 120 0 0 25 0 1 0 1797544622 80064512 18239 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19547 18239 145 145 0 19402 0 [pid=10560] vsize: 78188 Current children cumulated CPU time (s) 1038.7 Current children cumulated vsize (Kb) 80312 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22513 0 0 0 104749 121 0 0 25 0 1 0 1797544622 80416768 18326 4294967295 134512640 135094434 3221224432 3221223024 134557018 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19633 18326 145 145 0 19488 0 [pid=10560] vsize: 78532 Current children cumulated CPU time (s) 1048.7 Current children cumulated vsize (Kb) 80656 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22601 0 0 0 105749 121 0 0 25 0 1 0 1797544622 80785408 18414 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19723 18414 145 145 0 19578 0 [pid=10560] vsize: 78892 Current children cumulated CPU time (s) 1058.7 Current children cumulated vsize (Kb) 81016 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22692 0 0 0 106747 122 0 0 25 0 1 0 1797544622 81149952 18505 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19812 18505 145 145 0 19667 0 [pid=10560] vsize: 79248 Current children cumulated CPU time (s) 1068.69 Current children cumulated vsize (Kb) 81372 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22764 0 0 0 107747 122 0 0 25 0 1 0 1797544622 81457152 18577 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19887 18577 145 145 0 19742 0 [pid=10560] vsize: 79548 Current children cumulated CPU time (s) 1078.69 Current children cumulated vsize (Kb) 81672 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22853 0 0 0 108746 123 0 0 25 0 1 0 1797544622 81829888 18666 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 19978 18666 145 145 0 19833 0 [pid=10560] vsize: 79912 Current children cumulated CPU time (s) 1088.69 Current children cumulated vsize (Kb) 82036 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 22913 0 0 0 109746 123 0 0 25 0 1 0 1797544622 82063360 18726 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20035 18726 145 145 0 19890 0 [pid=10560] vsize: 80140 Current children cumulated CPU time (s) 1098.69 Current children cumulated vsize (Kb) 82264 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23003 0 0 0 110745 124 0 0 25 0 1 0 1797544622 82427904 18816 4294967295 134512640 135094434 3221224432 3221223104 134555547 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20124 18816 145 145 0 19979 0 [pid=10560] vsize: 80496 Current children cumulated CPU time (s) 1108.69 Current children cumulated vsize (Kb) 82620 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 111743 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1118.68 Current children cumulated vsize (Kb) 82748 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 112744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1128.69 Current children cumulated vsize (Kb) 82748 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 113744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1138.69 Current children cumulated vsize (Kb) 82748 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 114744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1148.69 Current children cumulated vsize (Kb) 82748 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 115744 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1158.69 Current children cumulated vsize (Kb) 82748 [startup+1170.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 116745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1168.7 Current children cumulated vsize (Kb) 82748 [startup+1180.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 117745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1178.7 Current children cumulated vsize (Kb) 82748 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 118745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1188.7 Current children cumulated vsize (Kb) 82748 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 119745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1198.7 Current children cumulated vsize (Kb) 82748 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 120745 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1208.7 Current children cumulated vsize (Kb) 82748 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 10560 Raw data (/proc/10556/stat): 10556 (minisat+_script) S 10555 10556 15400 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1797544617 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/10556/statm): 531 226 485 147 0 384 0 [pid=10556] vsize: 2124 Raw data (/proc/10560/stat): 10560 (minisat+_64-bit) R 10556 10556 15400 0 -1 0 23099 0 0 0 120746 125 0 0 25 0 1 0 1797544622 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/10560/statm): 20156 18848 145 145 0 20011 0 [pid=10560] vsize: 80624 Current children cumulated CPU time (s) 1208.71 Current children cumulated vsize (Kb) 82748 Sending SIGTERM to -10556 Sleeping 2 seconds One traced child (pid=10556) ended because it received signal 15 (SIGTERM) One traced child (pid=10560) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.75 CPU user time (s): 1207.46 CPU system time (s): 1.2898 CPU usage (%): 99.8851 Max. virtual memory (cumulated for all children) (Kb): 82748
ERROR: no interpretation found !