Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-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.06 |
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 wulflinc12 THE 2005-09-19 18:23:03 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3019 boxname=wulflinc12 idbench=675 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 581d778a36086562107993896110e0a2 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-mod008.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-mod008.opb IDLAUNCH: 3019 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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: 921480 kB Buffers: 37032 kB Cached: 43888 kB SwapCached: 544 kB Active: 59020 kB Inactive: 24480 kB HighTotal: 131008 kB HighFree: 86492 kB LowTotal: 903652 kB LowFree: 834988 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5884 kB Slab: 23880 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 18:43:14 (client local time) WITH STATUS 10 IN 1208.74 SECONDS stats: 3019 7 1208.74 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/4238/stat): 4238 (minisat+_script) R 4237 4238 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1793785736 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/4238/statm): 174 3 169 147 0 27 0 [pid=4238] 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=4239 New process pid=4240 New process pid=4241 One traced child (pid=4240) 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=4241) exited with status: 0 One traced child (pid=4239) exited with status: 0 New process pid=4242 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-mod008.opb [startup+10.0039 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 4707 0 0 0 971 15 0 0 25 0 1 0 1793785741 5906432 1286 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 1442 1286 145 145 0 1297 0 [pid=4242] vsize: 5768 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 7892 [startup+20.0048 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9637 0 0 0 1933 34 0 0 25 0 1 0 1793785741 28651520 5748 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 6995 5748 145 145 0 6850 0 [pid=4242] vsize: 27980 Current children cumulated CPU time (s) 19.69 Current children cumulated vsize (Kb) 30104 [startup+30.0057 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9682 0 0 0 2931 35 0 0 25 0 1 0 1793785741 28831744 5793 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 7039 5793 145 145 0 6894 0 [pid=4242] vsize: 28156 Current children cumulated CPU time (s) 29.68 Current children cumulated vsize (Kb) 30280 [startup+40.0065 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9818 0 0 0 3928 36 0 0 25 0 1 0 1793785741 29372416 5929 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 7171 5929 145 145 0 7026 0 [pid=4242] vsize: 28684 Current children cumulated CPU time (s) 39.66 Current children cumulated vsize (Kb) 30808 [startup+50.0083 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 9978 0 0 0 4925 38 0 0 25 0 1 0 1793785741 30007296 6089 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 7326 6089 145 145 0 7181 0 [pid=4242] vsize: 29304 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 31428 [startup+60.0092 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10242 0 0 0 5923 39 0 0 25 0 1 0 1793785741 30896128 6311 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7543 6311 145 145 0 7398 0 [pid=4242] vsize: 30172 Current children cumulated CPU time (s) 59.64 Current children cumulated vsize (Kb) 32296 [startup+70.01 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10265 0 0 0 6922 40 0 0 25 0 1 0 1793785741 30986240 6334 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7565 6334 145 145 0 7420 0 [pid=4242] vsize: 30260 Current children cumulated CPU time (s) 69.64 Current children cumulated vsize (Kb) 32384 [startup+80.0109 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10309 0 0 0 7921 40 0 0 25 0 1 0 1793785741 31227904 6378 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 7624 6378 145 145 0 7479 0 [pid=4242] vsize: 30496 Current children cumulated CPU time (s) 79.63 Current children cumulated vsize (Kb) 32620 [startup+90.0127 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10426 0 0 0 8919 41 0 0 25 0 1 0 1793785741 31432704 6430 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7674 6430 145 145 0 7529 0 [pid=4242] vsize: 30696 Current children cumulated CPU time (s) 89.62 Current children cumulated vsize (Kb) 32820 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10497 0 0 0 9919 42 0 0 25 0 1 0 1793785741 31727616 6501 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7746 6501 145 145 0 7601 0 [pid=4242] vsize: 30984 Current children cumulated CPU time (s) 99.63 Current children cumulated vsize (Kb) 33108 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10599 0 0 0 10917 42 0 0 25 0 1 0 1793785741 32141312 6603 4294967295 134512640 135094434 3221224432 3221223088 134557914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7847 6603 145 145 0 7702 0 [pid=4242] vsize: 31388 Current children cumulated CPU time (s) 109.61 Current children cumulated vsize (Kb) 33512 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 10854 0 0 0 11914 43 0 0 25 0 1 0 1793785741 32653312 6731 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 7972 6731 145 145 0 7827 0 [pid=4242] vsize: 31888 Current children cumulated CPU time (s) 119.59 Current children cumulated vsize (Kb) 34012 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11015 0 0 0 12912 45 0 0 25 0 1 0 1793785741 33361920 6892 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8145 6892 145 145 0 8000 0 [pid=4242] vsize: 32580 Current children cumulated CPU time (s) 129.59 Current children cumulated vsize (Kb) 34704 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11244 0 0 0 13909 47 0 0 25 0 1 0 1793785741 34033664 7057 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8309 7057 145 145 0 8164 0 [pid=4242] vsize: 33236 Current children cumulated CPU time (s) 139.58 Current children cumulated vsize (Kb) 35360 [startup+150.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11312 0 0 0 14908 47 0 0 25 0 1 0 1793785741 34308096 7125 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8376 7125 145 145 0 8231 0 [pid=4242] vsize: 33504 Current children cumulated CPU time (s) 149.57 Current children cumulated vsize (Kb) 35628 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11405 0 0 0 15906 48 0 0 25 0 1 0 1793785741 34684928 7218 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8468 7218 145 145 0 8323 0 [pid=4242] vsize: 33872 Current children cumulated CPU time (s) 159.56 Current children cumulated vsize (Kb) 35996 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11481 0 0 0 16905 48 0 0 25 0 1 0 1793785741 34959360 7294 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8535 7294 145 145 0 8390 0 [pid=4242] vsize: 34140 Current children cumulated CPU time (s) 169.55 Current children cumulated vsize (Kb) 36264 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11521 0 0 0 17905 49 0 0 25 0 1 0 1793785741 35119104 7334 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8574 7334 145 145 0 8429 0 [pid=4242] vsize: 34296 Current children cumulated CPU time (s) 179.56 Current children cumulated vsize (Kb) 36420 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11735 0 0 0 18901 50 0 0 25 0 1 0 1793785741 35991552 7548 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8787 7548 145 145 0 8642 0 [pid=4242] vsize: 35148 Current children cumulated CPU time (s) 189.53 Current children cumulated vsize (Kb) 37272 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 11937 0 0 0 19899 52 0 0 25 0 1 0 1793785741 36814848 7750 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 8988 7750 145 145 0 8843 0 [pid=4242] vsize: 35952 Current children cumulated CPU time (s) 199.53 Current children cumulated vsize (Kb) 38076 [startup+210.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12310 0 0 0 20892 55 0 0 25 0 1 0 1793785741 38338560 8123 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 9360 8123 145 145 0 9215 0 [pid=4242] vsize: 37440 Current children cumulated CPU time (s) 209.49 Current children cumulated vsize (Kb) 39564 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12691 0 0 0 21888 57 0 0 25 0 1 0 1793785741 39895040 8504 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 9740 8504 145 145 0 9595 0 [pid=4242] vsize: 38960 Current children cumulated CPU time (s) 219.47 Current children cumulated vsize (Kb) 41084 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 12955 0 0 0 22884 59 0 0 25 0 1 0 1793785741 40972288 8768 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 10003 8768 145 145 0 9858 0 [pid=4242] vsize: 40012 Current children cumulated CPU time (s) 229.45 Current children cumulated vsize (Kb) 42136 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13306 0 0 0 23878 61 0 0 25 0 1 0 1793785741 42405888 9119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 10353 9119 145 145 0 10208 0 [pid=4242] vsize: 41412 Current children cumulated CPU time (s) 239.41 Current children cumulated vsize (Kb) 43536 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13416 0 0 0 24877 61 0 0 25 0 1 0 1793785741 42983424 9229 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 10494 9229 145 145 0 10349 0 [pid=4242] vsize: 41976 Current children cumulated CPU time (s) 249.4 Current children cumulated vsize (Kb) 44100 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13708 0 0 0 25872 63 0 0 25 0 1 0 1793785741 44175360 9521 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 10785 9521 145 145 0 10640 0 [pid=4242] vsize: 43140 Current children cumulated CPU time (s) 259.37 Current children cumulated vsize (Kb) 45264 [startup+270.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 13985 0 0 0 26869 65 0 0 25 0 1 0 1793785741 45301760 9798 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 11060 9798 145 145 0 10915 0 [pid=4242] vsize: 44240 Current children cumulated CPU time (s) 269.36 Current children cumulated vsize (Kb) 46364 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14224 0 0 0 27865 67 0 0 25 0 1 0 1793785741 46280704 10037 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 11299 10037 145 145 0 11154 0 [pid=4242] vsize: 45196 Current children cumulated CPU time (s) 279.34 Current children cumulated vsize (Kb) 47320 [startup+290.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14467 0 0 0 28862 69 0 0 25 0 1 0 1793785741 47271936 10280 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 11541 10280 145 145 0 11396 0 [pid=4242] vsize: 46164 Current children cumulated CPU time (s) 289.33 Current children cumulated vsize (Kb) 48288 [startup+300.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14640 0 0 0 29859 70 0 0 25 0 1 0 1793785741 47972352 10453 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 11712 10453 145 145 0 11567 0 [pid=4242] vsize: 46848 Current children cumulated CPU time (s) 299.31 Current children cumulated vsize (Kb) 48972 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 14953 0 0 0 30856 71 0 0 25 0 1 0 1793785741 49254400 10766 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 12025 10766 145 145 0 11880 0 [pid=4242] vsize: 48100 Current children cumulated CPU time (s) 309.29 Current children cumulated vsize (Kb) 50224 [startup+320.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15146 0 0 0 31854 73 0 0 25 0 1 0 1793785741 50036736 10959 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 12216 10959 145 145 0 12071 0 [pid=4242] vsize: 48864 Current children cumulated CPU time (s) 319.29 Current children cumulated vsize (Kb) 50988 [startup+330.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15347 0 0 0 32849 76 0 0 25 0 1 0 1793785741 50855936 11160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 12416 11160 145 145 0 12271 0 [pid=4242] vsize: 49664 Current children cumulated CPU time (s) 329.27 Current children cumulated vsize (Kb) 51788 [startup+340.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15582 0 0 0 33844 78 0 0 25 0 1 0 1793785741 51810304 11395 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 12649 11395 145 145 0 12504 0 [pid=4242] vsize: 50596 Current children cumulated CPU time (s) 339.24 Current children cumulated vsize (Kb) 52720 [startup+350.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15802 0 0 0 34840 80 0 0 25 0 1 0 1793785741 52707328 11615 4294967295 134512640 135094434 3221224432 3221223056 134557645 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 12868 11615 145 145 0 12723 0 [pid=4242] vsize: 51472 Current children cumulated CPU time (s) 349.22 Current children cumulated vsize (Kb) 53596 [startup+360.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 15983 0 0 0 35837 82 0 0 25 0 1 0 1793785741 53440512 11796 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 13047 11796 145 145 0 12902 0 [pid=4242] vsize: 52188 Current children cumulated CPU time (s) 359.21 Current children cumulated vsize (Kb) 54312 [startup+370.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16179 0 0 0 36834 84 0 0 25 0 1 0 1793785741 54239232 11992 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 13242 11992 145 145 0 13097 0 [pid=4242] vsize: 52968 Current children cumulated CPU time (s) 369.2 Current children cumulated vsize (Kb) 55092 [startup+380.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16367 0 0 0 37832 84 0 0 25 0 1 0 1793785741 55013376 12180 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 13431 12180 145 145 0 13286 0 [pid=4242] vsize: 53724 Current children cumulated CPU time (s) 379.18 Current children cumulated vsize (Kb) 55848 [startup+390.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16551 0 0 0 38829 86 0 0 25 0 1 0 1793785741 55758848 12364 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 13613 12364 145 145 0 13468 0 [pid=4242] vsize: 54452 Current children cumulated CPU time (s) 389.17 Current children cumulated vsize (Kb) 56576 [startup+400.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 16810 0 0 0 39824 88 0 0 25 0 1 0 1793785741 56811520 12623 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 13870 12623 145 145 0 13725 0 [pid=4242] vsize: 55480 Current children cumulated CPU time (s) 399.14 Current children cumulated vsize (Kb) 57604 [startup+410.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17042 0 0 0 40821 90 0 0 25 0 1 0 1793785741 57757696 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 14101 12855 145 145 0 13956 0 [pid=4242] vsize: 56404 Current children cumulated CPU time (s) 409.13 Current children cumulated vsize (Kb) 58528 [startup+420.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17175 0 0 0 41819 91 0 0 25 0 1 0 1793785741 58298368 12988 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 14233 12988 145 145 0 14088 0 [pid=4242] vsize: 56932 Current children cumulated CPU time (s) 419.12 Current children cumulated vsize (Kb) 59056 [startup+430.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17267 0 0 0 42817 92 0 0 25 0 1 0 1793785741 58671104 13080 4294967295 134512640 135094434 3221224432 3221223120 134554739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 14324 13080 145 145 0 14179 0 [pid=4242] vsize: 57296 Current children cumulated CPU time (s) 429.11 Current children cumulated vsize (Kb) 59420 [startup+440.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17525 0 0 0 43812 94 0 0 25 0 1 0 1793785741 59719680 13338 4294967295 134512640 135094434 3221224432 3221223056 134557642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 14580 13338 145 145 0 14435 0 [pid=4242] vsize: 58320 Current children cumulated CPU time (s) 439.08 Current children cumulated vsize (Kb) 60444 [startup+450.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 17753 0 0 0 44808 96 0 0 25 0 1 0 1793785741 60645376 13566 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 14806 13566 145 145 0 14661 0 [pid=4242] vsize: 59224 Current children cumulated CPU time (s) 449.06 Current children cumulated vsize (Kb) 61348 [startup+460.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18057 0 0 0 45803 98 0 0 25 0 1 0 1793785741 61882368 13870 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 15108 13870 145 145 0 14963 0 [pid=4242] vsize: 60432 Current children cumulated CPU time (s) 459.03 Current children cumulated vsize (Kb) 62556 [startup+470.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18380 0 0 0 46796 101 0 0 25 0 1 0 1793785741 63205376 14193 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 15431 14193 145 145 0 15286 0 [pid=4242] vsize: 61724 Current children cumulated CPU time (s) 468.99 Current children cumulated vsize (Kb) 63848 [startup+480.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18496 0 0 0 47795 101 0 0 25 0 1 0 1793785741 63676416 14309 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 15546 14309 145 145 0 15401 0 [pid=4242] vsize: 62184 Current children cumulated CPU time (s) 478.98 Current children cumulated vsize (Kb) 64308 [startup+490.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18612 0 0 0 48793 102 0 0 25 0 1 0 1793785741 64147456 14425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 15661 14425 145 145 0 15516 0 [pid=4242] vsize: 62644 Current children cumulated CPU time (s) 488.97 Current children cumulated vsize (Kb) 64768 [startup+500.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 18819 0 0 0 49790 103 0 0 25 0 1 0 1793785741 64987136 14632 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 15866 14632 145 145 0 15721 0 [pid=4242] vsize: 63464 Current children cumulated CPU time (s) 498.95 Current children cumulated vsize (Kb) 65588 [startup+510.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19019 0 0 0 50787 104 0 0 25 0 1 0 1793785741 65806336 14832 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16066 14832 145 145 0 15921 0 [pid=4242] vsize: 64264 Current children cumulated CPU time (s) 508.93 Current children cumulated vsize (Kb) 66388 [startup+520.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19146 0 0 0 51786 105 0 0 25 0 1 0 1793785741 66322432 14959 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16192 14959 145 145 0 16047 0 [pid=4242] vsize: 64768 Current children cumulated CPU time (s) 518.93 Current children cumulated vsize (Kb) 66892 [startup+530.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19247 0 0 0 52785 106 0 0 25 0 1 0 1793785741 67108864 15060 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16384 15060 145 145 0 16239 0 [pid=4242] vsize: 65536 Current children cumulated CPU time (s) 528.93 Current children cumulated vsize (Kb) 67660 [startup+540.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19361 0 0 0 53783 106 0 0 25 0 1 0 1793785741 67571712 15174 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16497 15174 145 145 0 16352 0 [pid=4242] vsize: 65988 Current children cumulated CPU time (s) 538.91 Current children cumulated vsize (Kb) 68112 [startup+550.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19484 0 0 0 54781 107 0 0 25 0 1 0 1793785741 68067328 15297 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16618 15297 145 145 0 16473 0 [pid=4242] vsize: 66472 Current children cumulated CPU time (s) 548.9 Current children cumulated vsize (Kb) 68596 [startup+560.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19594 0 0 0 55779 108 0 0 25 0 1 0 1793785741 68517888 15407 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16728 15407 145 145 0 16583 0 [pid=4242] vsize: 66912 Current children cumulated CPU time (s) 558.89 Current children cumulated vsize (Kb) 69036 [startup+570.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19649 0 0 0 56779 109 0 0 25 0 1 0 1793785741 68739072 15462 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16782 15462 145 145 0 16637 0 [pid=4242] vsize: 67128 Current children cumulated CPU time (s) 568.9 Current children cumulated vsize (Kb) 69252 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19691 0 0 0 57778 109 0 0 25 0 1 0 1793785741 68911104 15504 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16824 15504 145 145 0 16679 0 [pid=4242] vsize: 67296 Current children cumulated CPU time (s) 578.89 Current children cumulated vsize (Kb) 69420 [startup+590.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19735 0 0 0 58777 109 0 0 25 0 1 0 1793785741 69091328 15548 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16868 15548 145 145 0 16723 0 [pid=4242] vsize: 67472 Current children cumulated CPU time (s) 588.88 Current children cumulated vsize (Kb) 69596 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19860 0 0 0 59775 111 0 0 25 0 1 0 1793785741 69599232 15673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 16992 15673 145 145 0 16847 0 [pid=4242] vsize: 67968 Current children cumulated CPU time (s) 598.88 Current children cumulated vsize (Kb) 70092 [startup+610.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 19972 0 0 0 60773 111 0 0 25 0 1 0 1793785741 70057984 15785 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17104 15785 145 145 0 16959 0 [pid=4242] vsize: 68416 Current children cumulated CPU time (s) 608.86 Current children cumulated vsize (Kb) 70540 [startup+620.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20079 0 0 0 61772 112 0 0 25 0 1 0 1793785741 70492160 15892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17210 15892 145 145 0 17065 0 [pid=4242] vsize: 68840 Current children cumulated CPU time (s) 618.86 Current children cumulated vsize (Kb) 70964 [startup+630.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20169 0 0 0 62771 113 0 0 25 0 1 0 1793785741 70868992 15982 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17302 15982 145 145 0 17157 0 [pid=4242] vsize: 69208 Current children cumulated CPU time (s) 628.86 Current children cumulated vsize (Kb) 71332 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20272 0 0 0 63771 113 0 0 25 0 1 0 1793785741 71278592 16085 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17402 16085 145 145 0 17257 0 [pid=4242] vsize: 69608 Current children cumulated CPU time (s) 638.86 Current children cumulated vsize (Kb) 71732 [startup+650.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) T 4238 4238 8263 0 -1 0 20406 0 0 0 64768 114 0 0 25 0 1 0 1793785741 71823360 16219 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17535 16219 145 145 0 17390 0 [pid=4242] vsize: 70140 Current children cumulated CPU time (s) 648.84 Current children cumulated vsize (Kb) 72264 [startup+660.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20498 0 0 0 65767 115 0 0 25 0 1 0 1793785741 72208384 16311 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17629 16311 145 145 0 17484 0 [pid=4242] vsize: 70516 Current children cumulated CPU time (s) 658.84 Current children cumulated vsize (Kb) 72640 [startup+670.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20605 0 0 0 66765 116 0 0 25 0 1 0 1793785741 72634368 16418 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17733 16418 145 145 0 17588 0 [pid=4242] vsize: 70932 Current children cumulated CPU time (s) 668.83 Current children cumulated vsize (Kb) 73056 [startup+680.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20697 0 0 0 67764 117 0 0 25 0 1 0 1793785741 73011200 16510 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17825 16510 145 145 0 17680 0 [pid=4242] vsize: 71300 Current children cumulated CPU time (s) 678.83 Current children cumulated vsize (Kb) 73424 [startup+690.069 s] Raw data (loadavg): 0.99 0.97 0.91 4/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20738 0 0 0 68764 117 0 0 25 0 1 0 1793785741 73179136 16551 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17866 16551 145 145 0 17721 0 [pid=4242] vsize: 71464 Current children cumulated CPU time (s) 688.83 Current children cumulated vsize (Kb) 73588 [startup+700.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20807 0 0 0 69763 118 0 0 25 0 1 0 1793785741 73453568 16620 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 17933 16620 145 145 0 17788 0 [pid=4242] vsize: 71732 Current children cumulated CPU time (s) 698.83 Current children cumulated vsize (Kb) 73856 [startup+710.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 20896 0 0 0 70762 118 0 0 25 0 1 0 1793785741 73818112 16709 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18022 16709 145 145 0 17877 0 [pid=4242] vsize: 72088 Current children cumulated CPU time (s) 708.82 Current children cumulated vsize (Kb) 74212 [startup+720.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21016 0 0 0 71760 119 0 0 25 0 1 0 1793785741 74305536 16829 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18141 16829 145 145 0 17996 0 [pid=4242] vsize: 72564 Current children cumulated CPU time (s) 718.81 Current children cumulated vsize (Kb) 74688 [startup+730.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21106 0 0 0 72758 120 0 0 25 0 1 0 1793785741 74670080 16919 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18230 16919 145 145 0 18085 0 [pid=4242] vsize: 72920 Current children cumulated CPU time (s) 728.8 Current children cumulated vsize (Kb) 75044 [startup+740.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21233 0 0 0 73756 121 0 0 25 0 1 0 1793785741 75190272 17046 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18357 17046 145 145 0 18212 0 [pid=4242] vsize: 73428 Current children cumulated CPU time (s) 738.79 Current children cumulated vsize (Kb) 75552 [startup+750.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21300 0 0 0 74755 122 0 0 25 0 1 0 1793785741 75468800 17113 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18425 17113 145 145 0 18280 0 [pid=4242] vsize: 73700 Current children cumulated CPU time (s) 748.79 Current children cumulated vsize (Kb) 75824 [startup+760.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21414 0 0 0 75753 122 0 0 25 0 1 0 1793785741 75931648 17227 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18538 17227 145 145 0 18393 0 [pid=4242] vsize: 74152 Current children cumulated CPU time (s) 758.77 Current children cumulated vsize (Kb) 76276 [startup+770.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21509 0 0 0 76752 123 0 0 25 0 1 0 1793785741 76333056 17322 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 18636 17322 145 145 0 18491 0 [pid=4242] vsize: 74544 Current children cumulated CPU time (s) 768.77 Current children cumulated vsize (Kb) 76668 [startup+780.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21550 0 0 0 77751 123 0 0 25 0 1 0 1793785741 76509184 17363 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18679 17363 145 145 0 18534 0 [pid=4242] vsize: 74716 Current children cumulated CPU time (s) 778.76 Current children cumulated vsize (Kb) 76840 [startup+790.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21587 0 0 0 78751 123 0 0 25 0 1 0 1793785741 76656640 17400 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18715 17400 145 145 0 18570 0 [pid=4242] vsize: 74860 Current children cumulated CPU time (s) 788.76 Current children cumulated vsize (Kb) 76984 [startup+800.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21634 0 0 0 79750 124 0 0 25 0 1 0 1793785741 76845056 17447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18761 17447 145 145 0 18616 0 [pid=4242] vsize: 75044 Current children cumulated CPU time (s) 798.76 Current children cumulated vsize (Kb) 77168 [startup+810.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21660 0 0 0 80750 125 0 0 25 0 1 0 1793785741 76951552 17473 4294967295 134512640 135094434 3221224432 3221223104 134556437 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18787 17473 145 145 0 18642 0 [pid=4242] vsize: 75148 Current children cumulated CPU time (s) 808.77 Current children cumulated vsize (Kb) 77272 [startup+820.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21681 0 0 0 81750 125 0 0 25 0 1 0 1793785741 77037568 17494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18808 17494 145 145 0 18663 0 [pid=4242] vsize: 75232 Current children cumulated CPU time (s) 818.77 Current children cumulated vsize (Kb) 77356 [startup+830.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21698 0 0 0 82750 125 0 0 25 0 1 0 1793785741 77103104 17511 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18824 17511 145 145 0 18679 0 [pid=4242] vsize: 75296 Current children cumulated CPU time (s) 828.77 Current children cumulated vsize (Kb) 77420 [startup+840.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21719 0 0 0 83750 125 0 0 25 0 1 0 1793785741 77189120 17532 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18845 17532 145 145 0 18700 0 [pid=4242] vsize: 75380 Current children cumulated CPU time (s) 838.77 Current children cumulated vsize (Kb) 77504 [startup+850.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21747 0 0 0 84750 125 0 0 25 0 1 0 1793785741 77303808 17560 4294967295 134512640 135094434 3221224432 3221223056 134562128 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18873 17560 145 145 0 18728 0 [pid=4242] vsize: 75492 Current children cumulated CPU time (s) 848.77 Current children cumulated vsize (Kb) 77616 [startup+860.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21770 0 0 0 85750 125 0 0 25 0 1 0 1793785741 77393920 17583 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18895 17583 145 145 0 18750 0 [pid=4242] vsize: 75580 Current children cumulated CPU time (s) 858.77 Current children cumulated vsize (Kb) 77704 [startup+870.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21786 0 0 0 86750 126 0 0 25 0 1 0 1793785741 77459456 17599 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18911 17599 145 145 0 18766 0 [pid=4242] vsize: 75644 Current children cumulated CPU time (s) 868.78 Current children cumulated vsize (Kb) 77768 [startup+880.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21806 0 0 0 87749 126 0 0 25 0 1 0 1793785741 77541376 17619 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18931 17619 145 145 0 18786 0 [pid=4242] vsize: 75724 Current children cumulated CPU time (s) 878.77 Current children cumulated vsize (Kb) 77848 [startup+890.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21845 0 0 0 88749 126 0 0 25 0 1 0 1793785741 77705216 17658 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18971 17658 145 145 0 18826 0 [pid=4242] vsize: 75884 Current children cumulated CPU time (s) 888.77 Current children cumulated vsize (Kb) 78008 [startup+900.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21860 0 0 0 89748 126 0 0 25 0 1 0 1793785741 77762560 17673 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 18985 17673 145 145 0 18840 0 [pid=4242] vsize: 75940 Current children cumulated CPU time (s) 898.76 Current children cumulated vsize (Kb) 78064 [startup+910.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21879 0 0 0 90748 127 0 0 25 0 1 0 1793785741 77840384 17692 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19004 17692 145 145 0 18859 0 [pid=4242] vsize: 76016 Current children cumulated CPU time (s) 908.77 Current children cumulated vsize (Kb) 78140 [startup+920.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21911 0 0 0 91747 128 0 0 25 0 1 0 1793785741 77967360 17724 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19035 17724 145 145 0 18890 0 [pid=4242] vsize: 76140 Current children cumulated CPU time (s) 918.77 Current children cumulated vsize (Kb) 78264 [startup+930.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21953 0 0 0 92746 129 0 0 25 0 1 0 1793785741 78143488 17766 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 19078 17766 145 145 0 18933 0 [pid=4242] vsize: 76312 Current children cumulated CPU time (s) 928.77 Current children cumulated vsize (Kb) 78436 [startup+940.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 21982 0 0 0 93744 129 0 0 25 0 1 0 1793785741 78262272 17795 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19107 17795 145 145 0 18962 0 [pid=4242] vsize: 76428 Current children cumulated CPU time (s) 938.75 Current children cumulated vsize (Kb) 78552 [startup+950.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22017 0 0 0 94744 130 0 0 25 0 1 0 1793785741 78401536 17830 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19141 17830 145 145 0 18996 0 [pid=4242] vsize: 76564 Current children cumulated CPU time (s) 948.76 Current children cumulated vsize (Kb) 78688 [startup+960.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22045 0 0 0 95743 130 0 0 25 0 1 0 1793785741 78516224 17858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19169 17858 145 145 0 19024 0 [pid=4242] vsize: 76676 Current children cumulated CPU time (s) 958.75 Current children cumulated vsize (Kb) 78800 [startup+970.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22068 0 0 0 96743 131 0 0 25 0 1 0 1793785741 78606336 17881 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19191 17881 145 145 0 19046 0 [pid=4242] vsize: 76764 Current children cumulated CPU time (s) 968.76 Current children cumulated vsize (Kb) 78888 [startup+980.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22092 0 0 0 97742 131 0 0 25 0 1 0 1793785741 78704640 17905 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19215 17905 145 145 0 19070 0 [pid=4242] vsize: 76860 Current children cumulated CPU time (s) 978.75 Current children cumulated vsize (Kb) 78984 [startup+990.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22115 0 0 0 98742 131 0 0 25 0 1 0 1793785741 78794752 17928 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19237 17928 145 145 0 19092 0 [pid=4242] vsize: 76948 Current children cumulated CPU time (s) 988.75 Current children cumulated vsize (Kb) 79072 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22134 0 0 0 99742 131 0 0 25 0 1 0 1793785741 78876672 17947 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19257 17947 145 145 0 19112 0 [pid=4242] vsize: 77028 Current children cumulated CPU time (s) 998.75 Current children cumulated vsize (Kb) 79152 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22162 0 0 0 100742 132 0 0 25 0 1 0 1793785741 78991360 17975 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19285 17975 145 145 0 19140 0 [pid=4242] vsize: 77140 Current children cumulated CPU time (s) 1008.76 Current children cumulated vsize (Kb) 79264 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22256 0 0 0 101741 132 0 0 25 0 1 0 1793785741 79368192 18069 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19377 18069 145 145 0 19232 0 [pid=4242] vsize: 77508 Current children cumulated CPU time (s) 1018.75 Current children cumulated vsize (Kb) 79632 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22390 0 0 0 102740 133 0 0 25 0 1 0 1793785741 79921152 18203 4294967295 134512640 135094434 3221224432 3221223104 134555260 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19512 18203 145 145 0 19367 0 [pid=4242] vsize: 78048 Current children cumulated CPU time (s) 1028.75 Current children cumulated vsize (Kb) 80172 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22478 0 0 0 103739 133 0 0 25 0 1 0 1793785741 80273408 18291 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19598 18291 145 145 0 19453 0 [pid=4242] vsize: 78392 Current children cumulated CPU time (s) 1038.74 Current children cumulated vsize (Kb) 80516 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22553 0 0 0 104738 134 0 0 25 0 1 0 1793785741 80584704 18366 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19674 18366 145 145 0 19529 0 [pid=4242] vsize: 78696 Current children cumulated CPU time (s) 1048.74 Current children cumulated vsize (Kb) 80820 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22665 0 0 0 105737 134 0 0 25 0 1 0 1793785741 81047552 18478 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19787 18478 145 145 0 19642 0 [pid=4242] vsize: 79148 Current children cumulated CPU time (s) 1058.73 Current children cumulated vsize (Kb) 81272 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22721 0 0 0 106736 135 0 0 25 0 1 0 1793785741 81268736 18534 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19841 18534 145 145 0 19696 0 [pid=4242] vsize: 79364 Current children cumulated CPU time (s) 1068.73 Current children cumulated vsize (Kb) 81488 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22797 0 0 0 107735 136 0 0 25 0 1 0 1793785741 81592320 18610 4294967295 134512640 135094434 3221224432 3221223024 134557013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 19920 18610 145 145 0 19775 0 [pid=4242] vsize: 79680 Current children cumulated CPU time (s) 1078.73 Current children cumulated vsize (Kb) 81804 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22886 0 0 0 108735 136 0 0 25 0 1 0 1793785741 81965056 18699 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 20011 18699 145 145 0 19866 0 [pid=4242] vsize: 80044 Current children cumulated CPU time (s) 1088.73 Current children cumulated vsize (Kb) 82168 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 22947 0 0 0 109735 136 0 0 25 0 1 0 1793785741 82198528 18760 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/4242/statm): 20068 18760 145 145 0 19923 0 [pid=4242] vsize: 80272 Current children cumulated CPU time (s) 1098.73 Current children cumulated vsize (Kb) 82396 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 110732 137 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1108.71 Current children cumulated vsize (Kb) 82748 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 111732 138 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1118.72 Current children cumulated vsize (Kb) 82748 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 112731 138 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1128.71 Current children cumulated vsize (Kb) 82748 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 113731 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1138.72 Current children cumulated vsize (Kb) 82748 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 114731 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1148.72 Current children cumulated vsize (Kb) 82748 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 115730 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1158.71 Current children cumulated vsize (Kb) 82748 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 116730 139 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1168.71 Current children cumulated vsize (Kb) 82748 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 117730 140 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1178.72 Current children cumulated vsize (Kb) 82748 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 118729 140 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1188.71 Current children cumulated vsize (Kb) 82748 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 119729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1198.72 Current children cumulated vsize (Kb) 82748 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 120729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1208.72 Current children cumulated vsize (Kb) 82748 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 4242 Raw data (/proc/4238/stat): 4238 (minisat+_script) S 4237 4238 8263 0 -1 0 289 239 0 0 0 1 0 1 17 0 1 0 1793785736 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/4238/statm): 531 226 485 147 0 384 0 [pid=4238] vsize: 2124 Raw data (/proc/4242/stat): 4242 (minisat+_64-bit) R 4238 4238 8263 0 -1 0 23099 0 0 0 120729 141 0 0 25 0 1 0 1793785741 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/4242/statm): 20156 18848 145 145 0 20011 0 [pid=4242] vsize: 80624 Current children cumulated CPU time (s) 1208.72 Current children cumulated vsize (Kb) 82748 Sending SIGTERM to -4238 Sleeping 2 seconds One traced child (pid=4238) ended because it received signal 15 (SIGTERM) One traced child (pid=4242) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.16 CPU time (s): 1208.74 CPU user time (s): 1207.29 CPU system time (s): 1.44778 CPU usage (%): 99.8829 Max. virtual memory (cumulated for all children) (Kb): 82748
ERROR: no interpretation found !