Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-mod008.opb |
MD5SUM | fbdb3cf321a85412feefcaac30780520 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 361 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 319 |
Biggest coefficient in the objective function | 87 |
Number of bits for the biggest coefficient in the objective function | 7 |
Sum of the numbers in the objective function | 23554 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 22000 |
Number of bits of the biggest number in a constraint | 15 |
Biggest sum of numbers in a constraint | 1027256 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.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 03:13:06 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2868 boxname=wulflinc12 idbench=524 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fbdb3cf321a85412feefcaac30780520 /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: 2868 /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: 881536 kB Buffers: 39604 kB Cached: 73616 kB SwapCached: 544 kB Active: 70608 kB Inactive: 54860 kB HighTotal: 131008 kB HighFree: 57372 kB LowTotal: 903652 kB LowFree: 824164 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 36 kB Writeback: 0 kB Mapped: 5884 kB Slab: 22192 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 03:33:16 (client local time) WITH STATUS 10 IN 1208.76 SECONDS stats: 2868 7 1208.76 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/29309/stat): 29309 (minisat+_script) R 29308 29309 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788325283 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/29309/statm): 174 3 169 147 0 27 0 [pid=29309] 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=29310 New process pid=29311 New process pid=29312 execve syscall for /bin/sed executable One traced child (pid=29311) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=29312) exited with status: 0 One traced child (pid=29310) exited with status: 0 New process pid=29313 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.0036 s] Raw data (loadavg): 0.96 1.08 1.05 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 4707 0 0 0 970 14 0 0 25 0 1 0 1788325288 5906432 1286 4294967295 134512640 135094434 3221224432 3221221728 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 1442 1286 145 145 0 1297 0 [pid=29313] vsize: 5768 Current children cumulated CPU time (s) 9.85 Current children cumulated vsize (Kb) 7892 [startup+20.0045 s] Raw data (loadavg): 0.97 1.08 1.05 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9625 0 0 0 1934 33 0 0 25 0 1 0 1788325288 28651520 5736 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 6995 5736 145 145 0 6850 0 [pid=29313] vsize: 27980 Current children cumulated CPU time (s) 19.68 Current children cumulated vsize (Kb) 30104 [startup+30.0053 s] Raw data (loadavg): 0.97 1.07 1.05 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9682 0 0 0 2932 33 0 0 25 0 1 0 1788325288 28831744 5793 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7039 5793 145 145 0 6894 0 [pid=29313] vsize: 28156 Current children cumulated CPU time (s) 29.66 Current children cumulated vsize (Kb) 30280 [startup+40.0072 s] Raw data (loadavg): 0.98 1.07 1.05 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9818 0 0 0 3929 35 0 0 25 0 1 0 1788325288 29372416 5929 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7171 5929 145 145 0 7026 0 [pid=29313] vsize: 28684 Current children cumulated CPU time (s) 39.65 Current children cumulated vsize (Kb) 30808 [startup+50.008 s] Raw data (loadavg): 0.98 1.07 1.05 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 9976 0 0 0 4926 36 0 0 25 0 1 0 1788325288 29999104 6087 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7324 6087 145 145 0 7179 0 [pid=29313] vsize: 29296 Current children cumulated CPU time (s) 49.63 Current children cumulated vsize (Kb) 31420 [startup+60.0088 s] Raw data (loadavg): 0.98 1.06 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10242 0 0 0 5924 36 0 0 25 0 1 0 1788325288 30896128 6311 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7543 6311 145 145 0 7398 0 [pid=29313] vsize: 30172 Current children cumulated CPU time (s) 59.61 Current children cumulated vsize (Kb) 32296 [startup+70.0107 s] Raw data (loadavg): 0.98 1.06 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10264 0 0 0 6925 36 0 0 25 0 1 0 1788325288 30982144 6333 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7564 6333 145 145 0 7419 0 [pid=29313] vsize: 30256 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 32380 [startup+80.0115 s] Raw data (loadavg): 0.99 1.06 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10309 0 0 0 7924 37 0 0 25 0 1 0 1788325288 31227904 6378 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 7624 6378 145 145 0 7479 0 [pid=29313] vsize: 30496 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 32620 [startup+90.0134 s] Raw data (loadavg): 0.99 1.06 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10424 0 0 0 8923 38 0 0 25 0 1 0 1788325288 31424512 6428 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7672 6428 145 145 0 7527 0 [pid=29313] vsize: 30688 Current children cumulated CPU time (s) 89.62 Current children cumulated vsize (Kb) 32812 [startup+100.014 s] Raw data (loadavg): 0.99 1.05 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10496 0 0 0 9922 38 0 0 25 0 1 0 1788325288 31723520 6500 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7745 6500 145 145 0 7600 0 [pid=29313] vsize: 30980 Current children cumulated CPU time (s) 99.61 Current children cumulated vsize (Kb) 33104 [startup+110.015 s] Raw data (loadavg): 0.99 1.05 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10587 0 0 0 10920 39 0 0 25 0 1 0 1788325288 32092160 6591 4294967295 134512640 135094434 3221224432 3221222976 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7835 6591 145 145 0 7690 0 [pid=29313] vsize: 31340 Current children cumulated CPU time (s) 109.6 Current children cumulated vsize (Kb) 33464 [startup+120.017 s] Raw data (loadavg): 0.99 1.05 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 10849 0 0 0 11917 40 0 0 25 0 1 0 1788325288 32632832 6726 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 7967 6726 145 145 0 7822 0 [pid=29313] vsize: 31868 Current children cumulated CPU time (s) 119.58 Current children cumulated vsize (Kb) 33992 [startup+130.018 s] Raw data (loadavg): 0.99 1.05 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11015 0 0 0 12915 42 0 0 25 0 1 0 1788325288 33361920 6892 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8145 6892 145 145 0 8000 0 [pid=29313] vsize: 32580 Current children cumulated CPU time (s) 129.58 Current children cumulated vsize (Kb) 34704 [startup+140.019 s] Raw data (loadavg): 0.99 1.05 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11238 0 0 0 13912 43 0 0 25 0 1 0 1788325288 34009088 7051 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8303 7051 145 145 0 8158 0 [pid=29313] vsize: 33212 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 35336 [startup+150.019 s] Raw data (loadavg): 0.99 1.04 1.04 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11293 0 0 0 14911 43 0 0 25 0 1 0 1788325288 34230272 7106 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8357 7106 145 145 0 8212 0 [pid=29313] vsize: 33428 Current children cumulated CPU time (s) 149.55 Current children cumulated vsize (Kb) 35552 [startup+160.02 s] Raw data (loadavg): 0.99 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11400 0 0 0 15910 44 0 0 25 0 1 0 1788325288 34664448 7213 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8463 7213 145 145 0 8318 0 [pid=29313] vsize: 33852 Current children cumulated CPU time (s) 159.55 Current children cumulated vsize (Kb) 35976 [startup+170.021 s] Raw data (loadavg): 0.99 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11465 0 0 0 16909 45 0 0 25 0 1 0 1788325288 34934784 7278 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8529 7278 145 145 0 8384 0 [pid=29313] vsize: 34116 Current children cumulated CPU time (s) 169.55 Current children cumulated vsize (Kb) 36240 [startup+180.022 s] Raw data (loadavg): 0.99 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11517 0 0 0 17908 45 0 0 25 0 1 0 1788325288 35106816 7330 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8571 7330 145 145 0 8426 0 [pid=29313] vsize: 34284 Current children cumulated CPU time (s) 179.54 Current children cumulated vsize (Kb) 36408 [startup+190.024 s] Raw data (loadavg): 0.99 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11687 0 0 0 18906 46 0 0 25 0 1 0 1788325288 35794944 7500 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8739 7500 145 145 0 8594 0 [pid=29313] vsize: 34956 Current children cumulated CPU time (s) 189.53 Current children cumulated vsize (Kb) 37080 [startup+200.025 s] Raw data (loadavg): 0.99 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 11898 0 0 0 19903 48 0 0 25 0 1 0 1788325288 36655104 7711 4294967295 134512640 135094434 3221224432 3221223104 134556523 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 8949 7711 145 145 0 8804 0 [pid=29313] vsize: 35796 Current children cumulated CPU time (s) 199.52 Current children cumulated vsize (Kb) 37920 [startup+210.025 s] Raw data (loadavg): 0.99 1.03 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12196 0 0 0 20898 50 0 0 25 0 1 0 1788325288 37871616 8009 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 9246 8009 145 145 0 9101 0 [pid=29313] vsize: 36984 Current children cumulated CPU time (s) 209.49 Current children cumulated vsize (Kb) 39108 [startup+220.027 s] Raw data (loadavg): 0.99 1.03 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12680 0 0 0 21892 52 0 0 25 0 1 0 1788325288 39849984 8493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 9729 8493 145 145 0 9584 0 [pid=29313] vsize: 38916 Current children cumulated CPU time (s) 219.45 Current children cumulated vsize (Kb) 41040 [startup+230.028 s] Raw data (loadavg): 0.99 1.03 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 12881 0 0 0 22889 54 0 0 25 0 1 0 1788325288 40669184 8694 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 9929 8694 145 145 0 9784 0 [pid=29313] vsize: 39716 Current children cumulated CPU time (s) 229.44 Current children cumulated vsize (Kb) 41840 [startup+240.029 s] Raw data (loadavg): 0.99 1.03 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13250 0 0 0 23883 57 0 0 25 0 1 0 1788325288 42176512 9063 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 10297 9063 145 145 0 10152 0 [pid=29313] vsize: 41188 Current children cumulated CPU time (s) 239.41 Current children cumulated vsize (Kb) 43312 [startup+250.03 s] Raw data (loadavg): 0.99 1.03 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13391 0 0 0 24882 58 0 0 25 0 1 0 1788325288 42881024 9204 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 10469 9204 145 145 0 10324 0 [pid=29313] vsize: 41876 Current children cumulated CPU time (s) 249.41 Current children cumulated vsize (Kb) 44000 [startup+260.031 s] Raw data (loadavg): 0.99 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) T 29309 29309 8263 0 -1 0 13606 0 0 0 25878 59 0 0 25 0 1 0 1788325288 43757568 9419 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/29313/statm): 10683 9419 145 145 0 10538 0 [pid=29313] vsize: 42732 Current children cumulated CPU time (s) 259.38 Current children cumulated vsize (Kb) 44856 [startup+270.031 s] Raw data (loadavg): 0.99 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 13907 0 0 0 26875 61 0 0 25 0 1 0 1788325288 44986368 9720 4294967295 134512640 135094434 3221224432 3221223024 134556870 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 10983 9720 145 145 0 10838 0 [pid=29313] vsize: 43932 Current children cumulated CPU time (s) 269.37 Current children cumulated vsize (Kb) 46056 [startup+280.032 s] Raw data (loadavg): 0.99 1.02 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14134 0 0 0 27872 62 0 0 25 0 1 0 1788325288 45912064 9947 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 11209 9947 145 145 0 11064 0 [pid=29313] vsize: 44836 Current children cumulated CPU time (s) 279.35 Current children cumulated vsize (Kb) 46960 [startup+290.034 s] Raw data (loadavg): 0.99 1.02 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14427 0 0 0 28868 64 0 0 25 0 1 0 1788325288 47108096 10240 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 11501 10240 145 145 0 11356 0 [pid=29313] vsize: 46004 Current children cumulated CPU time (s) 289.33 Current children cumulated vsize (Kb) 48128 [startup+300.035 s] Raw data (loadavg): 0.99 1.02 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14584 0 0 0 29867 65 0 0 25 0 1 0 1788325288 47751168 10397 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 11658 10397 145 145 0 11513 0 [pid=29313] vsize: 46632 Current children cumulated CPU time (s) 299.33 Current children cumulated vsize (Kb) 48756 [startup+310.036 s] Raw data (loadavg): 1.07 1.04 1.03 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 14876 0 0 0 30863 66 0 0 25 0 1 0 1788325288 48934912 10689 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 11947 10689 145 145 0 11802 0 [pid=29313] vsize: 47788 Current children cumulated CPU time (s) 309.3 Current children cumulated vsize (Kb) 49912 [startup+320.037 s] Raw data (loadavg): 1.06 1.04 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15077 0 0 0 31861 67 0 0 25 0 1 0 1788325288 49762304 10890 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 12149 10890 145 145 0 12004 0 [pid=29313] vsize: 48596 Current children cumulated CPU time (s) 319.29 Current children cumulated vsize (Kb) 50720 [startup+330.037 s] Raw data (loadavg): 1.05 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15277 0 0 0 32857 68 0 0 25 0 1 0 1788325288 50573312 11090 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 12347 11090 145 145 0 12202 0 [pid=29313] vsize: 49388 Current children cumulated CPU time (s) 329.26 Current children cumulated vsize (Kb) 51512 [startup+340.038 s] Raw data (loadavg): 1.04 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15493 0 0 0 33853 70 0 0 25 0 1 0 1788325288 51449856 11306 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 12561 11306 145 145 0 12416 0 [pid=29313] vsize: 50244 Current children cumulated CPU time (s) 339.24 Current children cumulated vsize (Kb) 52368 [startup+350.039 s] Raw data (loadavg): 1.03 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15732 0 0 0 34850 71 0 0 25 0 1 0 1788325288 52420608 11545 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 12798 11545 145 145 0 12653 0 [pid=29313] vsize: 51192 Current children cumulated CPU time (s) 349.22 Current children cumulated vsize (Kb) 53316 [startup+360.04 s] Raw data (loadavg): 1.03 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 15893 0 0 0 35847 73 0 0 25 0 1 0 1788325288 53075968 11706 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 12958 11706 145 145 0 12813 0 [pid=29313] vsize: 51832 Current children cumulated CPU time (s) 359.21 Current children cumulated vsize (Kb) 53956 [startup+370.042 s] Raw data (loadavg): 1.02 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16099 0 0 0 36844 74 0 0 25 0 1 0 1788325288 53915648 11912 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 13163 11912 145 145 0 13018 0 [pid=29313] vsize: 52652 Current children cumulated CPU time (s) 369.19 Current children cumulated vsize (Kb) 54776 [startup+380.043 s] Raw data (loadavg): 1.02 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16309 0 0 0 37841 76 0 0 25 0 1 0 1788325288 54771712 12122 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 13372 12122 145 145 0 13227 0 [pid=29313] vsize: 53488 Current children cumulated CPU time (s) 379.18 Current children cumulated vsize (Kb) 55612 [startup+390.045 s] Raw data (loadavg): 1.02 1.03 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16457 0 0 0 38840 76 0 0 25 0 1 0 1788325288 55377920 12270 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 13520 12270 145 145 0 13375 0 [pid=29313] vsize: 54080 Current children cumulated CPU time (s) 389.17 Current children cumulated vsize (Kb) 56204 [startup+400.045 s] Raw data (loadavg): 1.01 1.02 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16700 0 0 0 39836 78 0 0 25 0 1 0 1788325288 56365056 12513 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 13761 12513 145 145 0 13616 0 [pid=29313] vsize: 55044 Current children cumulated CPU time (s) 399.15 Current children cumulated vsize (Kb) 57168 [startup+410.045 s] Raw data (loadavg): 1.01 1.02 1.02 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 16931 0 0 0 40830 80 0 0 25 0 1 0 1788325288 57307136 12744 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 13991 12744 145 145 0 13846 0 [pid=29313] vsize: 55964 Current children cumulated CPU time (s) 409.11 Current children cumulated vsize (Kb) 58088 [startup+420.046 s] Raw data (loadavg): 1.01 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17128 0 0 0 41827 82 0 0 25 0 1 0 1788325288 58105856 12941 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 14186 12941 145 145 0 14041 0 [pid=29313] vsize: 56744 Current children cumulated CPU time (s) 419.1 Current children cumulated vsize (Kb) 58868 [startup+430.047 s] Raw data (loadavg): 1.01 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17191 0 0 0 42825 83 0 0 25 0 1 0 1788325288 58359808 13004 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 14248 13004 145 145 0 14103 0 [pid=29313] vsize: 56992 Current children cumulated CPU time (s) 429.09 Current children cumulated vsize (Kb) 59116 [startup+440.048 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17386 0 0 0 43822 84 0 0 25 0 1 0 1788325288 59154432 13199 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 14442 13199 145 145 0 14297 0 [pid=29313] vsize: 57768 Current children cumulated CPU time (s) 439.07 Current children cumulated vsize (Kb) 59892 [startup+450.049 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17623 0 0 0 44818 86 0 0 25 0 1 0 1788325288 60116992 13436 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 14677 13436 145 145 0 14532 0 [pid=29313] vsize: 58708 Current children cumulated CPU time (s) 449.05 Current children cumulated vsize (Kb) 60832 [startup+460.049 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 17927 0 0 0 45813 88 0 0 25 0 1 0 1788325288 61353984 13740 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 14979 13740 145 145 0 14834 0 [pid=29313] vsize: 59916 Current children cumulated CPU time (s) 459.02 Current children cumulated vsize (Kb) 62040 [startup+470.05 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18186 0 0 0 46809 91 0 0 25 0 1 0 1788325288 62410752 13999 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 15237 13999 145 145 0 15092 0 [pid=29313] vsize: 60948 Current children cumulated CPU time (s) 469.01 Current children cumulated vsize (Kb) 63072 [startup+480.051 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18471 0 0 0 47805 93 0 0 25 0 1 0 1788325288 63574016 14284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 15521 14284 145 145 0 15376 0 [pid=29313] vsize: 62084 Current children cumulated CPU time (s) 478.99 Current children cumulated vsize (Kb) 64208 [startup+490.053 s] Raw data (loadavg): 1.00 1.02 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18512 0 0 0 48805 93 0 0 25 0 1 0 1788325288 63737856 14325 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 15561 14325 145 145 0 15416 0 [pid=29313] vsize: 62244 Current children cumulated CPU time (s) 488.99 Current children cumulated vsize (Kb) 64368 [startup+500.054 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18685 0 0 0 49802 94 0 0 25 0 1 0 1788325288 64442368 14498 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 15733 14498 145 145 0 15588 0 [pid=29313] vsize: 62932 Current children cumulated CPU time (s) 498.97 Current children cumulated vsize (Kb) 65056 [startup+510.055 s] Raw data (loadavg): 1.00 1.01 1.01 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 18896 0 0 0 50799 96 0 0 25 0 1 0 1788325288 65302528 14709 4294967295 134512640 135094434 3221224432 3221223024 134556793 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 15943 14709 145 145 0 15798 0 [pid=29313] vsize: 63772 Current children cumulated CPU time (s) 508.96 Current children cumulated vsize (Kb) 65896 [startup+520.055 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19062 0 0 0 51796 96 0 0 25 0 1 0 1788325288 65978368 14875 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16108 14875 145 145 0 15963 0 [pid=29313] vsize: 64432 Current children cumulated CPU time (s) 518.93 Current children cumulated vsize (Kb) 66556 [startup+530.056 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19223 0 0 0 52794 97 0 0 25 0 1 0 1788325288 67006464 15036 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16359 15036 145 145 0 16214 0 [pid=29313] vsize: 65436 Current children cumulated CPU time (s) 528.92 Current children cumulated vsize (Kb) 67560 [startup+540.057 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19274 0 0 0 53793 98 0 0 25 0 1 0 1788325288 67223552 15087 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16412 15087 145 145 0 16267 0 [pid=29313] vsize: 65648 Current children cumulated CPU time (s) 538.92 Current children cumulated vsize (Kb) 67772 [startup+550.058 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19386 0 0 0 54792 98 0 0 25 0 1 0 1788325288 67674112 15199 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16522 15199 145 145 0 16377 0 [pid=29313] vsize: 66088 Current children cumulated CPU time (s) 548.91 Current children cumulated vsize (Kb) 68212 [startup+560.059 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19512 0 0 0 55790 99 0 0 25 0 1 0 1788325288 68182016 15325 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16646 15325 145 145 0 16501 0 [pid=29313] vsize: 66584 Current children cumulated CPU time (s) 558.9 Current children cumulated vsize (Kb) 68708 [startup+570.06 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19612 0 0 0 56789 99 0 0 25 0 1 0 1788325288 68591616 15425 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16746 15425 145 145 0 16601 0 [pid=29313] vsize: 66984 Current children cumulated CPU time (s) 568.89 Current children cumulated vsize (Kb) 69108 [startup+580.06 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19660 0 0 0 57789 99 0 0 25 0 1 0 1788325288 68784128 15473 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16793 15473 145 145 0 16648 0 [pid=29313] vsize: 67172 Current children cumulated CPU time (s) 578.89 Current children cumulated vsize (Kb) 69296 [startup+590.061 s] Raw data (loadavg): 1.00 1.01 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19704 0 0 0 58789 99 0 0 25 0 1 0 1788325288 68964352 15517 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16837 15517 145 145 0 16692 0 [pid=29313] vsize: 67348 Current children cumulated CPU time (s) 588.89 Current children cumulated vsize (Kb) 69472 [startup+600.062 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19768 0 0 0 59788 100 0 0 25 0 1 0 1788325288 69226496 15581 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 16901 15581 145 145 0 16756 0 [pid=29313] vsize: 67604 Current children cumulated CPU time (s) 598.89 Current children cumulated vsize (Kb) 69728 [startup+610.063 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19898 0 0 0 60787 100 0 0 25 0 1 0 1788325288 69754880 15711 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17030 15711 145 145 0 16885 0 [pid=29313] vsize: 68120 Current children cumulated CPU time (s) 608.88 Current children cumulated vsize (Kb) 70244 [startup+620.064 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 19992 0 0 0 61786 101 0 0 25 0 1 0 1788325288 70139904 15805 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17124 15805 145 145 0 16979 0 [pid=29313] vsize: 68496 Current children cumulated CPU time (s) 618.88 Current children cumulated vsize (Kb) 70620 [startup+630.065 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20110 0 0 0 62784 102 0 0 25 0 1 0 1788325288 70619136 15923 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17241 15923 145 145 0 17096 0 [pid=29313] vsize: 68964 Current children cumulated CPU time (s) 628.87 Current children cumulated vsize (Kb) 71088 [startup+640.067 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20197 0 0 0 63783 102 0 0 25 0 1 0 1788325288 70971392 16010 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17327 16010 145 145 0 17182 0 [pid=29313] vsize: 69308 Current children cumulated CPU time (s) 638.86 Current children cumulated vsize (Kb) 71432 [startup+650.067 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20311 0 0 0 64781 103 0 0 25 0 1 0 1788325288 71438336 16124 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17441 16124 145 145 0 17296 0 [pid=29313] vsize: 69764 Current children cumulated CPU time (s) 648.85 Current children cumulated vsize (Kb) 71888 [startup+660.068 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20435 0 0 0 65780 104 0 0 25 0 1 0 1788325288 71942144 16248 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17564 16248 145 145 0 17419 0 [pid=29313] vsize: 70256 Current children cumulated CPU time (s) 658.85 Current children cumulated vsize (Kb) 72380 [startup+670.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20520 0 0 0 66780 104 0 0 25 0 1 0 1788325288 72290304 16333 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17649 16333 145 145 0 17504 0 [pid=29313] vsize: 70596 Current children cumulated CPU time (s) 668.85 Current children cumulated vsize (Kb) 72720 [startup+680.071 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20631 0 0 0 67779 104 0 0 25 0 1 0 1788325288 72740864 16444 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17759 16444 145 145 0 17614 0 [pid=29313] vsize: 71036 Current children cumulated CPU time (s) 678.84 Current children cumulated vsize (Kb) 73160 [startup+690.073 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20710 0 0 0 68778 105 0 0 25 0 1 0 1788325288 73072640 16523 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17840 16523 145 145 0 17695 0 [pid=29313] vsize: 71360 Current children cumulated CPU time (s) 688.84 Current children cumulated vsize (Kb) 73484 [startup+700.075 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20745 0 0 0 69778 105 0 0 25 0 1 0 1788325288 73207808 16558 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17873 16558 145 145 0 17728 0 [pid=29313] vsize: 71492 Current children cumulated CPU time (s) 698.84 Current children cumulated vsize (Kb) 73616 [startup+710.074 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20815 0 0 0 70777 105 0 0 25 0 1 0 1788325288 73494528 16628 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 17943 16628 145 145 0 17798 0 [pid=29313] vsize: 71772 Current children cumulated CPU time (s) 708.83 Current children cumulated vsize (Kb) 73896 [startup+720.075 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 20910 0 0 0 71776 106 0 0 25 0 1 0 1788325288 73875456 16723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18036 16723 145 145 0 17891 0 [pid=29313] vsize: 72144 Current children cumulated CPU time (s) 718.83 Current children cumulated vsize (Kb) 74268 [startup+730.076 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21022 0 0 0 72775 107 0 0 25 0 1 0 1788325288 74330112 16835 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18147 16835 145 145 0 18002 0 [pid=29313] vsize: 72588 Current children cumulated CPU time (s) 728.83 Current children cumulated vsize (Kb) 74712 [startup+740.078 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21121 0 0 0 73773 107 0 0 25 0 1 0 1788325288 74731520 16934 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18245 16934 145 145 0 18100 0 [pid=29313] vsize: 72980 Current children cumulated CPU time (s) 738.81 Current children cumulated vsize (Kb) 75104 [startup+750.079 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21240 0 0 0 74772 108 0 0 25 0 1 0 1788325288 75218944 17053 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18364 17053 145 145 0 18219 0 [pid=29313] vsize: 73456 Current children cumulated CPU time (s) 748.81 Current children cumulated vsize (Kb) 75580 [startup+760.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21309 0 0 0 75771 108 0 0 25 0 1 0 1788325288 75509760 17122 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18435 17122 145 145 0 18290 0 [pid=29313] vsize: 73740 Current children cumulated CPU time (s) 758.8 Current children cumulated vsize (Kb) 75864 [startup+770.08 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21429 0 0 0 76769 109 0 0 25 0 1 0 1788325288 76005376 17242 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18556 17242 145 145 0 18411 0 [pid=29313] vsize: 74224 Current children cumulated CPU time (s) 768.79 Current children cumulated vsize (Kb) 76348 [startup+780.081 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21514 0 0 0 77769 109 0 0 25 0 1 0 1788325288 76353536 17327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18641 17327 145 145 0 18496 0 [pid=29313] vsize: 74564 Current children cumulated CPU time (s) 778.79 Current children cumulated vsize (Kb) 76688 [startup+790.083 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21558 0 0 0 78768 109 0 0 25 0 1 0 1788325288 76537856 17371 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18686 17371 145 145 0 18541 0 [pid=29313] vsize: 74744 Current children cumulated CPU time (s) 788.78 Current children cumulated vsize (Kb) 76868 [startup+800.084 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21593 0 0 0 79768 110 0 0 25 0 1 0 1788325288 76681216 17406 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18721 17406 145 145 0 18576 0 [pid=29313] vsize: 74884 Current children cumulated CPU time (s) 798.79 Current children cumulated vsize (Kb) 77008 [startup+810.085 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21637 0 0 0 80767 110 0 0 25 0 1 0 1788325288 76857344 17450 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18764 17450 145 145 0 18619 0 [pid=29313] vsize: 75056 Current children cumulated CPU time (s) 808.78 Current children cumulated vsize (Kb) 77180 [startup+820.086 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21663 0 0 0 81766 111 0 0 25 0 1 0 1788325288 76963840 17476 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18790 17476 145 145 0 18645 0 [pid=29313] vsize: 75160 Current children cumulated CPU time (s) 818.78 Current children cumulated vsize (Kb) 77284 [startup+830.086 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21682 0 0 0 82766 111 0 0 25 0 1 0 1788325288 77041664 17495 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18809 17495 145 145 0 18664 0 [pid=29313] vsize: 75236 Current children cumulated CPU time (s) 828.78 Current children cumulated vsize (Kb) 77360 [startup+840.088 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21698 0 0 0 83766 111 0 0 25 0 1 0 1788325288 77103104 17511 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18824 17511 145 145 0 18679 0 [pid=29313] vsize: 75296 Current children cumulated CPU time (s) 838.78 Current children cumulated vsize (Kb) 77420 [startup+850.089 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21719 0 0 0 84766 111 0 0 25 0 1 0 1788325288 77189120 17532 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 18845 17532 145 145 0 18700 0 [pid=29313] vsize: 75380 Current children cumulated CPU time (s) 848.78 Current children cumulated vsize (Kb) 77504 [startup+860.089 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21749 0 0 0 85765 112 0 0 25 0 1 0 1788325288 77312000 17562 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18875 17562 145 145 0 18730 0 [pid=29313] vsize: 75500 Current children cumulated CPU time (s) 858.78 Current children cumulated vsize (Kb) 77624 [startup+870.091 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21774 0 0 0 86765 112 0 0 25 0 1 0 1788325288 77410304 17587 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18899 17587 145 145 0 18754 0 [pid=29313] vsize: 75596 Current children cumulated CPU time (s) 868.78 Current children cumulated vsize (Kb) 77720 [startup+880.093 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21787 0 0 0 87764 112 0 0 25 0 1 0 1788325288 77463552 17600 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18912 17600 145 145 0 18767 0 [pid=29313] vsize: 75648 Current children cumulated CPU time (s) 878.77 Current children cumulated vsize (Kb) 77772 [startup+890.093 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21806 0 0 0 88764 113 0 0 25 0 1 0 1788325288 77541376 17619 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18931 17619 145 145 0 18786 0 [pid=29313] vsize: 75724 Current children cumulated CPU time (s) 888.78 Current children cumulated vsize (Kb) 77848 [startup+900.094 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21846 0 0 0 89763 114 0 0 25 0 1 0 1788325288 77709312 17659 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18972 17659 145 145 0 18827 0 [pid=29313] vsize: 75888 Current children cumulated CPU time (s) 898.78 Current children cumulated vsize (Kb) 78012 [startup+910.096 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21860 0 0 0 90762 115 0 0 25 0 1 0 1788325288 77762560 17673 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 18985 17673 145 145 0 18840 0 [pid=29313] vsize: 75940 Current children cumulated CPU time (s) 908.78 Current children cumulated vsize (Kb) 78064 [startup+920.097 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21882 0 0 0 91761 115 0 0 25 0 1 0 1788325288 77852672 17695 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 19007 17695 145 145 0 18862 0 [pid=29313] vsize: 76028 Current children cumulated CPU time (s) 918.77 Current children cumulated vsize (Kb) 78152 [startup+930.098 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21914 0 0 0 92760 116 0 0 25 0 1 0 1788325288 77979648 17727 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 19038 17727 145 145 0 18893 0 [pid=29313] vsize: 76152 Current children cumulated CPU time (s) 928.77 Current children cumulated vsize (Kb) 78276 [startup+940.099 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21958 0 0 0 93757 118 0 0 25 0 1 0 1788325288 78163968 17771 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 19083 17771 145 145 0 18938 0 [pid=29313] vsize: 76332 Current children cumulated CPU time (s) 938.76 Current children cumulated vsize (Kb) 78456 [startup+950.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 21984 0 0 0 94756 119 0 0 25 0 1 0 1788325288 78270464 17797 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 19109 17797 145 145 0 18964 0 [pid=29313] vsize: 76436 Current children cumulated CPU time (s) 948.76 Current children cumulated vsize (Kb) 78560 [startup+960.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22019 0 0 0 95756 119 0 0 25 0 1 0 1788325288 78409728 17832 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19143 17832 145 145 0 18998 0 [pid=29313] vsize: 76572 Current children cumulated CPU time (s) 958.76 Current children cumulated vsize (Kb) 78696 [startup+970.102 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22046 0 0 0 96755 119 0 0 25 0 1 0 1788325288 78520320 17859 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19170 17859 145 145 0 19025 0 [pid=29313] vsize: 76680 Current children cumulated CPU time (s) 968.75 Current children cumulated vsize (Kb) 78804 [startup+980.103 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22069 0 0 0 97755 120 0 0 25 0 1 0 1788325288 78610432 17882 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19192 17882 145 145 0 19047 0 [pid=29313] vsize: 76768 Current children cumulated CPU time (s) 978.76 Current children cumulated vsize (Kb) 78892 [startup+990.104 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22093 0 0 0 98755 120 0 0 25 0 1 0 1788325288 78708736 17906 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19216 17906 145 145 0 19071 0 [pid=29313] vsize: 76864 Current children cumulated CPU time (s) 988.76 Current children cumulated vsize (Kb) 78988 [startup+1000.1 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22116 0 0 0 99755 120 0 0 25 0 1 0 1788325288 78798848 17929 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19238 17929 145 145 0 19093 0 [pid=29313] vsize: 76952 Current children cumulated CPU time (s) 998.76 Current children cumulated vsize (Kb) 79076 [startup+1010.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22135 0 0 0 100755 120 0 0 25 0 1 0 1788325288 78880768 17948 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19258 17948 145 145 0 19113 0 [pid=29313] vsize: 77032 Current children cumulated CPU time (s) 1008.76 Current children cumulated vsize (Kb) 79156 [startup+1020.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22162 0 0 0 101755 120 0 0 25 0 1 0 1788325288 78991360 17975 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19285 17975 145 145 0 19140 0 [pid=29313] vsize: 77140 Current children cumulated CPU time (s) 1018.76 Current children cumulated vsize (Kb) 79264 [startup+1030.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22260 0 0 0 102753 121 0 0 25 0 1 0 1788325288 79384576 18073 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19381 18073 145 145 0 19236 0 [pid=29313] vsize: 77524 Current children cumulated CPU time (s) 1028.75 Current children cumulated vsize (Kb) 79648 [startup+1040.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22392 0 0 0 103752 121 0 0 25 0 1 0 1788325288 79925248 18205 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19513 18205 145 145 0 19368 0 [pid=29313] vsize: 78052 Current children cumulated CPU time (s) 1038.74 Current children cumulated vsize (Kb) 80176 [startup+1050.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22478 0 0 0 104751 122 0 0 25 0 1 0 1788325288 80273408 18291 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19598 18291 145 145 0 19453 0 [pid=29313] vsize: 78392 Current children cumulated CPU time (s) 1048.74 Current children cumulated vsize (Kb) 80516 [startup+1060.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22553 0 0 0 105751 122 0 0 25 0 1 0 1788325288 80584704 18366 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19674 18366 145 145 0 19529 0 [pid=29313] vsize: 78696 Current children cumulated CPU time (s) 1058.74 Current children cumulated vsize (Kb) 80820 [startup+1070.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22660 0 0 0 106750 123 0 0 25 0 1 0 1788325288 81022976 18473 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19781 18473 145 145 0 19636 0 [pid=29313] vsize: 79124 Current children cumulated CPU time (s) 1068.74 Current children cumulated vsize (Kb) 81248 [startup+1080.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22721 0 0 0 107748 123 0 0 25 0 1 0 1788325288 81268736 18534 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/29313/statm): 19841 18534 145 145 0 19696 0 [pid=29313] vsize: 79364 Current children cumulated CPU time (s) 1078.72 Current children cumulated vsize (Kb) 81488 [startup+1090.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22796 0 0 0 108746 124 0 0 25 0 1 0 1788325288 81588224 18609 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 19919 18609 145 145 0 19774 0 [pid=29313] vsize: 79676 Current children cumulated CPU time (s) 1088.71 Current children cumulated vsize (Kb) 81800 [startup+1100.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22882 0 0 0 109746 125 0 0 25 0 1 0 1788325288 81940480 18695 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20005 18695 145 145 0 19860 0 [pid=29313] vsize: 80020 Current children cumulated CPU time (s) 1098.72 Current children cumulated vsize (Kb) 82144 [startup+1110.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 22946 0 0 0 110746 125 0 0 25 0 1 0 1788325288 82198528 18759 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20068 18759 145 145 0 19923 0 [pid=29313] vsize: 80272 Current children cumulated CPU time (s) 1108.72 Current children cumulated vsize (Kb) 82396 [startup+1120.11 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 111743 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1118.7 Current children cumulated vsize (Kb) 82748 [startup+1130.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 112743 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1128.7 Current children cumulated vsize (Kb) 82748 [startup+1140.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 113744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1138.71 Current children cumulated vsize (Kb) 82748 [startup+1150.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 114744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1148.71 Current children cumulated vsize (Kb) 82748 [startup+1160.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 115744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557302 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1158.71 Current children cumulated vsize (Kb) 82748 [startup+1170.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 116744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1168.71 Current children cumulated vsize (Kb) 82748 [startup+1180.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 117744 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1178.71 Current children cumulated vsize (Kb) 82748 [startup+1190.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 118745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1188.72 Current children cumulated vsize (Kb) 82748 [startup+1200.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 119745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1198.72 Current children cumulated vsize (Kb) 82748 [startup+1210.12 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 120745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] 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): 1.00 1.00 1.00 2/57 29313 Raw data (/proc/29309/stat): 29309 (minisat+_script) S 29308 29309 8263 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788325283 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/29309/statm): 531 226 485 147 0 384 0 [pid=29309] vsize: 2124 Raw data (/proc/29313/stat): 29313 (minisat+_64-bit) R 29309 29309 8263 0 -1 0 23099 0 0 0 120745 126 0 0 25 0 1 0 1788325288 82558976 18848 4294967295 134512640 135094434 3221224432 3221223056 134562161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/29313/statm): 20156 18848 145 145 0 20011 0 [pid=29313] vsize: 80624 Current children cumulated CPU time (s) 1208.72 Current children cumulated vsize (Kb) 82748 Sending SIGTERM to -29309 Sleeping 2 seconds One traced child (pid=29309) ended because it received signal 15 (SIGTERM) One traced child (pid=29313) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.16 CPU time (s): 1208.76 CPU user time (s): 1207.46 CPU system time (s): 1.2978 CPU usage (%): 99.8838 Max. virtual memory (cumulated for all children) (Kb): 82748
ERROR: no interpretation found !