Name | web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.5:100.opb |
MD5SUM | dd81121db7c1c4b8597dd9571c707a87 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 3 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 372 |
Biggest coefficient in the objective function | 220 |
Number of bits for the biggest coefficient in the objective function | 8 |
Sum of the numbers in the objective function | 983 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 220 |
Number of bits of the biggest number in a constraint | 8 |
Biggest sum of numbers in a constraint | 983 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 19.3841 |
Number of variables | 372 |
Total number of constraints | 792 |
Number of constraints which are clauses | 345 |
Number of constraints which are cardinality constraints (but not clauses) | 447 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 18 |
LAUNCH ON wulflinc27 THE 2005-09-18 19:09:28 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2736 boxname=wulflinc27 idbench=392 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: dd81121db7c1c4b8597dd9571c707a87 /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb IDLAUNCH: 2736 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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: 910912 kB Buffers: 36040 kB Cached: 55608 kB SwapCached: 764 kB Active: 66908 kB Inactive: 27388 kB HighTotal: 131008 kB HighFree: 72828 kB LowTotal: 903652 kB LowFree: 838084 kB SwapTotal: 2097892 kB SwapFree: 2096616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5724 kB Slab: 23912 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:29:38 (client local time) WITH STATUS 10 IN 1208.63 SECONDS stats: 2736 7 1208.63 10
c Parsing PB file... c Converting 420 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................... c ---[ 85]---> BDD-cost: 17 c ---[ 84]---> BDD-cost: 23 c ---[ 83]---> BDD-cost: 29 c ---[ 82]---> BDD-cost: 35 c ---[ 81]---> BDD-cost: 35 c ---[ 80]---> BDD-cost: 32 c ---[ 79]---> BDD-cost: 32 c ---[ 78]---> BDD-cost: 26 c ---[ 77]---> BDD-cost: 20 c ---[ 76]---> BDD-cost: 14 c ---[ 75]---> BDD-cost: 20 c ---[ 74]---> BDD-cost: 26 c ---[ 73]---> BDD-cost: 32 c ---[ 72]---> BDD-cost: 35 c ---[ 71]---> BDD-cost: 35 c ---[ 70]---> BDD-cost: 32 c ---[ 69]---> BDD-cost: 35 c ---[ 68]---> BDD-cost: 26 c ---[ 67]---> BDD-cost: 23 c ---[ 66]---> BDD-cost: 17 c ---[ 65]---> BDD-cost: 18 c ---[ 64]---> BDD-cost: 26 c ---[ 63]---> BDD-cost: 32 c ---[ 62]---> BDD-cost: 38 c ---[ 61]---> BDD-cost: 44 c ---[ 60]---> BDD-cost: 35 c ---[ 59]---> BDD-cost: 38 c ---[ 58]---> BDD-cost: 32 c ---[ 57]---> BDD-cost: 26 c ---[ 56]---> BDD-cost: 17 c ---[ 55]---> BDD-cost: 14 c ---[ 54]---> BDD-cost: 23 c ---[ 53]---> BDD-cost: 32 c ---[ 52]---> BDD-cost: 44 c ---[ 51]---> BDD-cost: 47 c ---[ 50]---> BDD-cost: 41 c ---[ 49]---> BDD-cost: 35 c ---[ 48]---> BDD-cost: 29 c ---[ 47]---> BDD-cost: 21 c ---[ 46]---> BDD-cost: 20 c ---[ 45]---> BDD-cost: 11 c ---[ 44]---> BDD-cost: 17 c ---[ 43]---> BDD-cost: 21 c ---[ 42]---> BDD-cost: 38 c ---[ 41]---> BDD-cost: 32 c ---[ 40]---> BDD-cost: 41 c ---[ 39]---> BDD-cost: 29 c ---[ 38]---> BDD-cost: 23 c ---[ 37]---> BDD-cost: 9 c ---[ 36]---> BDD-cost: 9 c ---[ 35]---> BDD-cost: 11 c ---[ 34]---> BDD-cost: 14 c ---[ 33]---> BDD-cost: 14 c ---[ 32]---> BDD-cost: 20 c ---[ 31]---> BDD-cost: 14 c ---[ 30]---> BDD-cost: 26 c ---[ 29]---> BDD-cost: 9 c ---[ 28]---> BDD-cost: 11 c ---[ 27]---> BDD-cost: 7 c ---[ 25]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 8 c ---[ 23]---> BDD-cost: 11 c ---[ 22]---> BDD-cost: 11 c ---[ 21]---> BDD-cost: 5 c ---[ 20]---> BDD-cost: 14 c ---[ 19]---> BDD-cost: 11 c ---[ 18]---> BDD-cost: 7 c ---[ 16]---> BDD-cost: 3 c ---[ 15]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 5 c ---[ 13]---> BDD-cost: 8 c ---[ 11]---> BDD-cost: 14 c ---[ 10]---> BDD-cost: 7 c ---[ 7]---> BDD-cost: 3 c ---[ 3]---> BDD-cost: 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4084 11649 | 1361 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 355[0m c ---[ 0]---> Sorter-cost:20800 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 39610 94771 | 13203 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 119[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 52 | 40635 97290 | 13545 47 509 10.8 | 0.000 % | c | 153 | 40635 97290 | 14899 148 2006 13.6 | 0.807 % | c | 303 | 40635 97290 | 16389 298 3680 12.3 | 0.807 % | c ============================================================================== c [1mFound solution: 93[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 335 | 40816 97778 | 13605 330 3969 12.0 | 0.807 % | c ============================================================================== c [1mFound solution: 74[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 381 | 40957 98168 | 13652 376 4254 11.3 | 0.807 % | c | 482 | 40957 98168 | 15017 477 6680 14.0 | 0.809 % | c ============================================================================== c [1mFound solution: 66[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 543 | 41021 98358 | 13673 538 7309 13.6 | 0.809 % | c | 643 | 41007 98330 | 15040 637 8156 12.8 | 0.847 % | c ============================================================================== c [1mFound solution: 39[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 741 | 41137 98688 | 13712 735 12723 17.3 | 0.847 % | c | 841 | 41137 98688 | 15083 835 14812 17.7 | 0.858 % | c | 991 | 41137 98688 | 16591 985 15900 16.1 | 0.858 % | c | 1216 | 41137 98688 | 18250 1210 24830 20.5 | 0.858 % | c ============================================================================== c [1mFound solution: 32[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1549 | 40826 98032 | 13608 1526 31796 20.8 | 0.858 % | c | 1649 | 40807 97993 | 14968 1625 32748 20.2 | 1.610 % | c | 1799 | 40807 97993 | 16465 1775 35020 19.7 | 1.610 % | c | 2024 | 40807 97993 | 18112 2000 57066 28.5 | 1.610 % | c | 2361 | 40157 96519 | 19923 2253 61245 27.2 | 2.962 % | c | 2870 | 40157 96519 | 21915 2762 71091 25.7 | 2.962 % | c | 3629 | 40157 96519 | 24107 3521 86728 24.6 | 2.962 % | c | 4768 | 40069 96331 | 26518 4641 109000 23.5 | 3.209 % | c | 6476 | 39881 95923 | 29169 6320 241528 38.2 | 3.710 % | c | 9040 | 39881 95923 | 32086 8884 558335 62.8 | 3.710 % | c | 12886 | 39881 95923 | 35295 12730 837536 65.8 | 3.710 % | c | 18654 | 39881 95923 | 38825 18498 1338946 72.4 | 3.710 % | c | 27303 | 39881 95923 | 42707 27147 2479319 91.3 | 3.710 % | c ============================================================================== c [1mFound solution: 31[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30230 | 39885 95933 | 13295 30074 2833854 94.2 | 3.710 % | c | 30330 | 39885 95933 | 14624 13138 1476713 112.4 | 3.714 % | c | 30481 | 39885 95933 | 16086 13289 1480028 111.4 | 3.714 % | c | 30709 | 39885 95933 | 17695 13517 1485023 109.9 | 3.714 % | c | 31046 | 39885 95933 | 19465 13854 1491450 107.7 | 3.714 % | c | 31552 | 39885 95933 | 21411 14360 1526895 106.3 | 3.714 % | c | 32311 | 39885 95933 | 23552 15119 1570893 103.9 | 3.714 % | c | 33452 | 39885 95933 | 25908 16260 1620404 99.7 | 3.714 % | c | 35160 | 39871 95901 | 28499 17966 1667556 92.8 | 3.734 % | c | 37722 | 39871 95901 | 31348 20528 1922784 93.7 | 3.734 % | c ============================================================================== c [1mFound solution: 30[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37876 | 39892 95963 | 13297 20682 1934151 93.5 | 3.734 % | c | 37977 | 39838 95840 | 14626 10433 624856 59.9 | 3.810 % | c | 38128 | 39838 95840 | 16089 10584 628193 59.4 | 3.810 % | c | 38354 | 39838 95840 | 17698 10810 630346 58.3 | 3.810 % | c | 38692 | 39838 95840 | 19468 11148 638017 57.2 | 3.810 % | c | 39198 | 39838 95840 | 21414 11654 656390 56.3 | 3.810 % | c | 39957 | 39820 95799 | 23556 12406 664944 53.6 | 3.835 % | c ============================================================================== c [1mFound solution: 25[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40470 | 39846 95875 | 13282 12919 696562 53.9 | 3.835 % | c | 40570 | 39846 95875 | 14610 13019 698367 53.6 | 3.837 % | c | 40720 | 39846 95875 | 16071 13169 700531 53.2 | 3.837 % | c | 40945 | 39846 95875 | 17678 13394 705284 52.7 | 3.837 % | c | 41282 | 39739 95631 | 19446 13723 724893 52.8 | 4.074 % | c | 41789 | 39739 95631 | 21390 14230 774776 54.4 | 4.074 % | c | 42549 | 39721 95589 | 23529 14989 793085 52.9 | 4.129 % | c | 43688 | 39721 95589 | 25882 16128 862249 53.5 | 4.129 % | c | 45397 | 39721 95589 | 28471 17837 943295 52.9 | 4.129 % | c | 47959 | 39721 95589 | 31318 20399 1340906 65.7 | 4.129 % | c | 51803 | 39721 95589 | 34450 24243 1730566 71.4 | 4.129 % | c ============================================================================== c [1mFound solution: 18[0m c ---[ 0]---> Sorter-cost: 1 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53697 | 39759 95694 | 13253 26132 1833701 70.2 | 4.129 % | c | 53798 | 39759 95694 | 14578 13167 983300 74.7 | 4.137 % | c | 53948 | 39721 95606 | 16036 13310 984452 74.0 | 4.197 % | c | 54173 | 39721 95606 | 17639 13535 995185 73.5 | 4.197 % | c | 54510 | 39721 95606 | 19403 13872 1004647 72.4 | 4.197 % | c ============================================================================== c [1mFound solution: 9[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54616 | 39766 95725 | 13255 13978 1006538 72.0 | 4.197 % | c | 54716 | 39748 95684 | 14580 14071 1007232 71.6 | 4.220 % | c | 54866 | 39748 95684 | 16038 14221 1012093 71.2 | 4.220 % | c | 55091 | 39742 95670 | 17642 14443 1014604 70.2 | 4.230 % | c | 55428 | 39738 95661 | 19406 14779 1023087 69.2 | 4.235 % | c | 55934 | 39738 95661 | 21347 15285 1037095 67.9 | 4.235 % | c | 56693 | 39738 95661 | 23482 16044 1092277 68.1 | 4.235 % | c | 57832 | 39738 95661 | 25830 17183 1134775 66.0 | 4.235 % | c | 59541 | 39738 95661 | 28413 18892 1247008 66.0 | 4.235 % | c | 62103 | 39738 95661 | 31254 21454 1403165 65.4 | 4.235 % | c | 65947 | 39738 95661 | 34380 25298 2020808 79.9 | 4.235 % | c | 71714 | 39738 95661 | 37818 31065 2590932 83.4 | 4.235 % | c | 80363 | 39738 95661 | 41599 39714 3547339 89.3 | 4.235 % | c | 93337 | 39738 95661 | 45759 19456 2317262 119.1 | 4.235 % | c | 112798 | 39738 95661 | 50335 38917 5379251 138.2 | 4.235 % | c | 141992 | 39716 95612 | 55369 26150 3557617 136.0 | 4.270 % | c | 185781 | 39640 95444 | 60906 27874 1990715 71.4 | 4.457 % | c | 251466 | 39640 95444 | 66997 44447 9458461 212.8 | 4.457 % |
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/9877/stat): 9877 (minisat+_script) R 9876 9877 28974 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843647058 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/9877/statm): 174 3 169 147 0 27 0 [pid=9877] 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=9878 New process pid=9879 New process pid=9880 execve syscall for /bin/sed executable One traced child (pid=9879) 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=9880) exited with status: 0 One traced child (pid=9878) exited with status: 0 New process pid=9881 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc27/normalized-10:10:4.5:0.5:100.opb [startup+10.0039 s] Raw data (loadavg): 0.90 0.95 0.90 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2087 0 0 0 978 9 0 0 25 0 1 0 1843647063 9379840 1987 4294967295 134512640 135094434 3221224432 3221223064 134562981 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 2290 1987 145 145 0 2145 0 [pid=9881] vsize: 9160 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 11284 [startup+20.0058 s] Raw data (loadavg): 0.91 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2558 0 0 0 1970 12 0 0 25 0 1 0 1843647063 11325440 2458 4294967295 134512640 135094434 3221224432 3221223104 134556327 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 2765 2458 145 145 0 2620 0 [pid=9881] vsize: 11060 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 13184 [startup+30.0076 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 2976 0 0 0 2961 16 0 0 25 0 1 0 1843647063 13017088 2876 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 3178 2876 145 145 0 3033 0 [pid=9881] vsize: 12712 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 14836 [startup+40.0084 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 3385 0 0 0 3954 19 0 0 25 0 1 0 1843647063 14757888 3285 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 3603 3285 145 145 0 3458 0 [pid=9881] vsize: 14412 Current children cumulated CPU time (s) 39.74 Current children cumulated vsize (Kb) 16536 [startup+50.0102 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 3773 0 0 0 4945 23 0 0 25 0 1 0 1843647063 16334848 3673 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 3988 3673 145 145 0 3843 0 [pid=9881] vsize: 15952 Current children cumulated CPU time (s) 49.69 Current children cumulated vsize (Kb) 18076 [startup+60.011 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4156 0 0 0 5937 27 0 0 25 0 1 0 1843647063 17891328 4056 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 4368 4056 145 145 0 4223 0 [pid=9881] vsize: 17472 Current children cumulated CPU time (s) 59.65 Current children cumulated vsize (Kb) 19596 [startup+70.0129 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4546 0 0 0 6930 31 0 0 25 0 1 0 1843647063 19480576 4446 4294967295 134512640 135094434 3221224432 3221223024 134557287 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 4756 4446 145 145 0 4611 0 [pid=9881] vsize: 19024 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 21148 [startup+80.0147 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 7922 34 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221222080 134562864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 79.57 Current children cumulated vsize (Kb) 22764 [startup+90.0155 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 8922 34 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 89.57 Current children cumulated vsize (Kb) 22764 [startup+100.016 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 9922 35 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 99.58 Current children cumulated vsize (Kb) 22764 [startup+110.018 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 10921 36 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 109.58 Current children cumulated vsize (Kb) 22764 [startup+120.019 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 11921 36 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 119.58 Current children cumulated vsize (Kb) 22764 [startup+130.02 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 12920 37 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 129.58 Current children cumulated vsize (Kb) 22764 [startup+140.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 13919 37 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 139.57 Current children cumulated vsize (Kb) 22764 [startup+150.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 14919 38 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 149.58 Current children cumulated vsize (Kb) 22764 [startup+160.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4953 0 0 0 15919 38 0 0 25 0 1 0 1843647063 21135360 4853 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4853 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 159.58 Current children cumulated vsize (Kb) 22764 [startup+170.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 4954 0 0 0 16918 39 0 0 25 0 1 0 1843647063 21135360 4854 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5160 4854 145 145 0 5015 0 [pid=9881] vsize: 20640 Current children cumulated CPU time (s) 169.58 Current children cumulated vsize (Kb) 22764 [startup+180.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5208 0 0 0 17913 41 0 0 25 0 1 0 1843647063 22286336 5108 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5441 5108 145 145 0 5296 0 [pid=9881] vsize: 21764 Current children cumulated CPU time (s) 179.55 Current children cumulated vsize (Kb) 23888 [startup+190.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5600 0 0 0 18906 44 0 0 25 0 1 0 1843647063 23875584 5500 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 5829 5500 145 145 0 5684 0 [pid=9881] vsize: 23316 Current children cumulated CPU time (s) 189.51 Current children cumulated vsize (Kb) 25440 [startup+200.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 5939 0 0 0 19899 47 0 0 25 0 1 0 1843647063 25251840 5839 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 6165 5839 145 145 0 6020 0 [pid=9881] vsize: 24660 Current children cumulated CPU time (s) 199.47 Current children cumulated vsize (Kb) 26784 [startup+210.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 6343 0 0 0 20891 51 0 0 25 0 1 0 1843647063 26898432 6243 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 6567 6243 145 145 0 6422 0 [pid=9881] vsize: 26268 Current children cumulated CPU time (s) 209.43 Current children cumulated vsize (Kb) 28392 [startup+220.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 6757 0 0 0 21881 56 0 0 25 0 1 0 1843647063 28581888 6657 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 6978 6657 145 145 0 6833 0 [pid=9881] vsize: 27912 Current children cumulated CPU time (s) 219.38 Current children cumulated vsize (Kb) 30036 [startup+230.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7184 0 0 0 22872 59 0 0 25 0 1 0 1843647063 30322688 7084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7403 7084 145 145 0 7258 0 [pid=9881] vsize: 29612 Current children cumulated CPU time (s) 229.32 Current children cumulated vsize (Kb) 31736 [startup+240.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 23870 61 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 239.32 Current children cumulated vsize (Kb) 32088 [startup+250.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 24870 61 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 249.32 Current children cumulated vsize (Kb) 32088 [startup+260.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 25869 62 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 259.32 Current children cumulated vsize (Kb) 32088 [startup+270.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 26869 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 269.33 Current children cumulated vsize (Kb) 32088 [startup+280.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 27868 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 279.32 Current children cumulated vsize (Kb) 32088 [startup+290.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 28868 63 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223104 134555821 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 289.32 Current children cumulated vsize (Kb) 32088 [startup+300.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7273 0 0 0 29867 64 0 0 25 0 1 0 1843647063 30683136 7173 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 7491 7173 145 145 0 7346 0 [pid=9881] vsize: 29964 Current children cumulated CPU time (s) 299.32 Current children cumulated vsize (Kb) 32088 [startup+310.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7448 0 0 0 30864 66 0 0 25 0 1 0 1843647063 31399936 7348 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 7666 7348 145 145 0 7521 0 [pid=9881] vsize: 30664 Current children cumulated CPU time (s) 309.31 Current children cumulated vsize (Kb) 32788 [startup+320.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 7855 0 0 0 31856 69 0 0 25 0 1 0 1843647063 33071104 7755 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 8074 7755 145 145 0 7929 0 [pid=9881] vsize: 32296 Current children cumulated CPU time (s) 319.26 Current children cumulated vsize (Kb) 34420 [startup+330.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8206 0 0 0 32849 72 0 0 18 0 1 0 1843647063 34508800 8106 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 8425 8106 145 145 0 8280 0 [pid=9881] vsize: 33700 Current children cumulated CPU time (s) 329.22 Current children cumulated vsize (Kb) 35824 [startup+340.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8580 0 0 0 33842 75 0 0 25 0 1 0 1843647063 36040704 8480 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 8799 8480 145 145 0 8654 0 [pid=9881] vsize: 35196 Current children cumulated CPU time (s) 339.18 Current children cumulated vsize (Kb) 37320 [startup+350.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 8958 0 0 0 34835 78 0 0 25 0 1 0 1843647063 37588992 8858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 9177 8858 145 145 0 9032 0 [pid=9881] vsize: 36708 Current children cumulated CPU time (s) 349.14 Current children cumulated vsize (Kb) 38832 [startup+360.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 9366 0 0 0 35826 82 0 0 25 0 1 0 1843647063 39260160 9266 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 9585 9266 145 145 0 9440 0 [pid=9881] vsize: 38340 Current children cumulated CPU time (s) 359.09 Current children cumulated vsize (Kb) 40464 [startup+370.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 9743 0 0 0 36818 85 0 0 25 0 1 0 1843647063 40800256 9643 4294967295 134512640 135094434 3221224432 3221222896 134781611 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 9961 9643 145 145 0 9816 0 [pid=9881] vsize: 39844 Current children cumulated CPU time (s) 369.04 Current children cumulated vsize (Kb) 41968 [startup+380.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) T 9877 9877 28974 0 -1 0 10183 0 0 0 37810 90 0 0 25 0 1 0 1843647063 42590208 10083 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/9881/statm): 10398 10083 145 145 0 10253 0 [pid=9881] vsize: 41592 Current children cumulated CPU time (s) 379.01 Current children cumulated vsize (Kb) 43716 [startup+390.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 10615 0 0 0 38803 93 0 0 25 0 1 0 1843647063 44351488 10515 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 10828 10515 145 145 0 10683 0 [pid=9881] vsize: 43312 Current children cumulated CPU time (s) 388.97 Current children cumulated vsize (Kb) 45436 [startup+400.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 39797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 398.95 Current children cumulated vsize (Kb) 47080 [startup+410.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 40797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 408.95 Current children cumulated vsize (Kb) 47080 [startup+420.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 41797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 418.95 Current children cumulated vsize (Kb) 47080 [startup+430.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 42797 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 428.95 Current children cumulated vsize (Kb) 47080 [startup+440.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 43798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 438.96 Current children cumulated vsize (Kb) 47080 [startup+450.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 44798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 448.96 Current children cumulated vsize (Kb) 47080 [startup+460.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 45798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 458.96 Current children cumulated vsize (Kb) 47080 [startup+470.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 46798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 468.96 Current children cumulated vsize (Kb) 47080 [startup+480.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 47798 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 478.96 Current children cumulated vsize (Kb) 47080 [startup+490.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 48799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 488.97 Current children cumulated vsize (Kb) 47080 [startup+500.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 49799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 498.97 Current children cumulated vsize (Kb) 47080 [startup+510.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 50799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 508.97 Current children cumulated vsize (Kb) 47080 [startup+520.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 51799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 518.97 Current children cumulated vsize (Kb) 47080 [startup+530.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 52799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 528.97 Current children cumulated vsize (Kb) 47080 [startup+540.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 53799 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 538.97 Current children cumulated vsize (Kb) 47080 [startup+550.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 54800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 548.98 Current children cumulated vsize (Kb) 47080 [startup+560.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 55800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 558.98 Current children cumulated vsize (Kb) 47080 [startup+570.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 56800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 568.98 Current children cumulated vsize (Kb) 47080 [startup+580.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 57800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 578.98 Current children cumulated vsize (Kb) 47080 [startup+590.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 58800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 588.98 Current children cumulated vsize (Kb) 47080 [startup+600.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 59800 97 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 598.98 Current children cumulated vsize (Kb) 47080 [startup+610.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 60801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 609 Current children cumulated vsize (Kb) 47080 [startup+620.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 61801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 619 Current children cumulated vsize (Kb) 47080 [startup+630.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 62801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 629 Current children cumulated vsize (Kb) 47080 [startup+640.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 63801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 639 Current children cumulated vsize (Kb) 47080 [startup+650.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 64801 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 649 Current children cumulated vsize (Kb) 47080 [startup+660.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 65802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 659.01 Current children cumulated vsize (Kb) 47080 [startup+670.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 66802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 669.01 Current children cumulated vsize (Kb) 47080 [startup+680.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 67802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 679.01 Current children cumulated vsize (Kb) 47080 [startup+690.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11028 0 0 0 68802 98 0 0 25 0 1 0 1843647063 46034944 10928 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11239 10928 145 145 0 11094 0 [pid=9881] vsize: 44956 Current children cumulated CPU time (s) 689.01 Current children cumulated vsize (Kb) 47080 [startup+700.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11081 0 0 0 69801 98 0 0 25 0 1 0 1843647063 46252032 10981 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11292 10981 145 145 0 11147 0 [pid=9881] vsize: 45168 Current children cumulated CPU time (s) 699 Current children cumulated vsize (Kb) 47292 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11413 0 0 0 70797 101 0 0 25 0 1 0 1843647063 47640576 11313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 11631 11313 145 145 0 11486 0 [pid=9881] vsize: 46524 Current children cumulated CPU time (s) 708.99 Current children cumulated vsize (Kb) 48648 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 11788 0 0 0 71790 104 0 0 25 0 1 0 1843647063 49160192 11688 4294967295 134512640 135094434 3221224432 3221223024 134557137 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 12002 11688 145 145 0 11857 0 [pid=9881] vsize: 48008 Current children cumulated CPU time (s) 718.95 Current children cumulated vsize (Kb) 50132 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12127 0 0 0 72784 106 0 0 25 0 1 0 1843647063 50540544 12027 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 12339 12027 145 145 0 12194 0 [pid=9881] vsize: 49356 Current children cumulated CPU time (s) 728.91 Current children cumulated vsize (Kb) 51480 [startup+740.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12449 0 0 0 73778 108 0 0 25 0 1 0 1843647063 51847168 12349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 12658 12349 145 145 0 12513 0 [pid=9881] vsize: 50632 Current children cumulated CPU time (s) 738.87 Current children cumulated vsize (Kb) 52756 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 12769 0 0 0 74772 111 0 0 25 0 1 0 1843647063 53153792 12669 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 12977 12669 145 145 0 12832 0 [pid=9881] vsize: 51908 Current children cumulated CPU time (s) 748.84 Current children cumulated vsize (Kb) 54032 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13075 0 0 0 75767 112 0 0 25 0 1 0 1843647063 54403072 12975 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13282 12975 145 145 0 13137 0 [pid=9881] vsize: 53128 Current children cumulated CPU time (s) 758.8 Current children cumulated vsize (Kb) 55252 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13357 0 0 0 76761 115 0 0 25 0 1 0 1843647063 55853056 13257 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13636 13257 145 145 0 13491 0 [pid=9881] vsize: 54544 Current children cumulated CPU time (s) 768.77 Current children cumulated vsize (Kb) 56668 [startup+780.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13650 0 0 0 77756 117 0 0 25 0 1 0 1843647063 57053184 13550 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13929 13550 145 145 0 13784 0 [pid=9881] vsize: 55716 Current children cumulated CPU time (s) 778.74 Current children cumulated vsize (Kb) 57840 [startup+790.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 78757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 788.75 Current children cumulated vsize (Kb) 57852 [startup+800.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 79757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 798.75 Current children cumulated vsize (Kb) 57852 [startup+810.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 80757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 808.75 Current children cumulated vsize (Kb) 57852 [startup+820.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 81757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223104 134555453 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 818.75 Current children cumulated vsize (Kb) 57852 [startup+830.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 82757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 828.75 Current children cumulated vsize (Kb) 57852 [startup+840.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 83757 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 838.75 Current children cumulated vsize (Kb) 57852 [startup+850.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 84758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 848.76 Current children cumulated vsize (Kb) 57852 [startup+860.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 85758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 858.76 Current children cumulated vsize (Kb) 57852 [startup+870.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 86758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 868.76 Current children cumulated vsize (Kb) 57852 [startup+880.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 87758 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221222896 134781535 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 878.76 Current children cumulated vsize (Kb) 57852 [startup+890.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 88759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 888.77 Current children cumulated vsize (Kb) 57852 [startup+900.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 89759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 898.77 Current children cumulated vsize (Kb) 57852 [startup+910.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 90759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 908.77 Current children cumulated vsize (Kb) 57852 [startup+920.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 91759 117 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 918.77 Current children cumulated vsize (Kb) 57852 [startup+930.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 92759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 928.78 Current children cumulated vsize (Kb) 57852 [startup+940.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 93759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 938.78 Current children cumulated vsize (Kb) 57852 [startup+950.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 94759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 948.78 Current children cumulated vsize (Kb) 57852 [startup+960.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 95759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 958.78 Current children cumulated vsize (Kb) 57852 [startup+970.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 96759 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 968.78 Current children cumulated vsize (Kb) 57852 [startup+980.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13653 0 0 0 97760 118 0 0 25 0 1 0 1843647063 57065472 13553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 13932 13553 145 145 0 13787 0 [pid=9881] vsize: 55728 Current children cumulated CPU time (s) 978.79 Current children cumulated vsize (Kb) 57852 [startup+990.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 13908 0 0 0 98753 121 0 0 25 0 1 0 1843647063 58109952 13808 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 14187 13808 145 145 0 14042 0 [pid=9881] vsize: 56748 Current children cumulated CPU time (s) 988.75 Current children cumulated vsize (Kb) 58872 [startup+1000.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 14249 0 0 0 99747 124 0 0 25 0 1 0 1843647063 59506688 14149 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 14528 14149 145 145 0 14383 0 [pid=9881] vsize: 58112 Current children cumulated CPU time (s) 998.72 Current children cumulated vsize (Kb) 60236 [startup+1010.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 14626 0 0 0 100739 127 0 0 25 0 1 0 1843647063 61050880 14526 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 14905 14526 145 145 0 14760 0 [pid=9881] vsize: 59620 Current children cumulated CPU time (s) 1008.67 Current children cumulated vsize (Kb) 61744 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15068 0 0 0 101731 130 0 0 25 0 1 0 1843647063 62853120 14968 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15345 14968 145 145 0 15200 0 [pid=9881] vsize: 61380 Current children cumulated CPU time (s) 1018.62 Current children cumulated vsize (Kb) 63504 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15435 0 0 0 102725 133 0 0 25 0 1 0 1843647063 64352256 15335 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15711 15335 145 145 0 15566 0 [pid=9881] vsize: 62844 Current children cumulated CPU time (s) 1028.59 Current children cumulated vsize (Kb) 64968 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 103721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1038.56 Current children cumulated vsize (Kb) 65768 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 104721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1048.56 Current children cumulated vsize (Kb) 65768 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 105721 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1058.56 Current children cumulated vsize (Kb) 65768 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 106722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223104 134556519 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1068.57 Current children cumulated vsize (Kb) 65768 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 107722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1078.57 Current children cumulated vsize (Kb) 65768 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 108722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223084 134781722 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1088.57 Current children cumulated vsize (Kb) 65768 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 109722 134 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1098.57 Current children cumulated vsize (Kb) 65768 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 110722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1108.58 Current children cumulated vsize (Kb) 65768 [startup+1120.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 111722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1118.58 Current children cumulated vsize (Kb) 65768 [startup+1130.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 112722 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1128.58 Current children cumulated vsize (Kb) 65768 [startup+1140.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 113723 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1138.59 Current children cumulated vsize (Kb) 65768 [startup+1150.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15636 0 0 0 114723 135 0 0 25 0 1 0 1843647063 65171456 15536 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15536 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1148.59 Current children cumulated vsize (Kb) 65768 [startup+1160.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 115723 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1158.59 Current children cumulated vsize (Kb) 65768 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 116723 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1168.59 Current children cumulated vsize (Kb) 65768 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 117724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1178.6 Current children cumulated vsize (Kb) 65768 [startup+1190.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 118724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1188.6 Current children cumulated vsize (Kb) 65768 [startup+1200.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 119724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1198.6 Current children cumulated vsize (Kb) 65768 [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 120724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1208.6 Current children cumulated vsize (Kb) 65768 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 9881 Raw data (/proc/9877/stat): 9877 (minisat+_script) S 9876 9877 28974 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1843647058 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/9877/statm): 531 226 485 147 0 384 0 [pid=9877] vsize: 2124 Raw data (/proc/9881/stat): 9881 (minisat+_64-bit) R 9877 9877 28974 0 -1 0 15637 0 0 0 120724 135 0 0 25 0 1 0 1843647063 65171456 15537 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9881/statm): 15911 15537 145 145 0 15766 0 [pid=9881] vsize: 63644 Current children cumulated CPU time (s) 1208.6 Current children cumulated vsize (Kb) 65768 Sending SIGTERM to -9877 Sleeping 2 seconds One traced child (pid=9877) ended because it received signal 15 (SIGTERM) One traced child (pid=9881) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.63 CPU user time (s): 1207.25 CPU system time (s): 1.38679 CPU usage (%): 99.8752 Max. virtual memory (cumulated for all children) (Kb): 65768
ERROR: no interpretation found !