Name | submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-cmb.opb |
MD5SUM | a8596c98551f801a6658f1ce91b33278 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1053 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 304 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 12887 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 12887 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 63.6713 |
Number of variables | 304 |
Total number of constraints | 671 |
Number of constraints which are clauses | 671 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 28 |
LAUNCH ON wulflinc19 THE 2005-09-18 18:10:56 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2596 boxname=wulflinc19 idbench=252 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a8596c98551f801a6658f1ce91b33278 /oldhome/oroussel/tmp/wulflinc19/normalized-cmb.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-cmb.opb IDLAUNCH: 2596 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 926432 kB Buffers: 34384 kB Cached: 46996 kB SwapCached: 832 kB Active: 60252 kB Inactive: 23688 kB HighTotal: 131008 kB HighFree: 83300 kB LowTotal: 903652 kB LowFree: 843132 kB SwapTotal: 2097892 kB SwapFree: 2096460 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5700 kB Slab: 18740 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:31:06 (client local time) WITH STATUS 10 IN 1208.94 SECONDS stats: 2596 7 1208.94 10
c Parsing PB file... c Converting 667 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 667 3359 | 222 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 1524[0m c ---[ 0]---> Sorter-cost:43621 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 105121 247278 | 35040 0 0 nan | 0.000 % | c | 103 | 104168 245118 | 38544 97 4313 44.5 | 0.665 % | c | 253 | 103349 243238 | 42398 229 8034 35.1 | 1.287 % | c | 479 | 103349 243238 | 46638 455 17849 39.2 | 1.287 % | c | 816 | 103349 243238 | 51302 792 23717 29.9 | 1.287 % | c | 1322 | 103349 243238 | 56432 1298 40177 31.0 | 1.287 % | c | 2083 | 103122 242717 | 62075 2058 75941 36.9 | 1.487 % | c | 3222 | 102780 241953 | 68283 3169 126886 40.0 | 1.754 % | c | 4932 | 102722 241821 | 75111 4870 197921 40.6 | 1.797 % | c | 7495 | 102722 241821 | 82622 7433 294908 39.7 | 1.797 % | c ============================================================================== c [1mFound solution: 1514[0m c ---[ 0]---> Sorter-cost:36082 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8239 | 189796 445156 | 63265 8177 316528 38.7 | 1.797 % | c | 8339 | 189796 445156 | 69591 8277 322185 38.9 | 1.049 % | c | 8490 | 189796 445156 | 76550 8428 326473 38.7 | 1.049 % | c | 8715 | 189774 445107 | 84205 8650 331229 38.3 | 1.059 % | c | 9052 | 189647 444838 | 92626 8982 333087 37.1 | 1.125 % | c | 9558 | 189568 444660 | 101888 9486 337879 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1498[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9601 | 189573 444797 | 63191 9529 339448 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1490[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9608 | 189907 445610 | 63302 9536 339814 35.6 | 1.152 % | c ============================================================================== c [1mFound solution: 1450[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9611 | 189928 445664 | 63309 9539 340630 35.7 | 1.152 % | c ============================================================================== c [1mFound solution: 1416[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9623 | 190264 446559 | 63421 9551 341049 35.7 | 1.152 % | c | 9724 | 190264 446559 | 69763 9652 348331 36.1 | 1.152 % | c | 9874 | 190264 446559 | 76739 9802 364696 37.2 | 1.152 % | c | 10099 | 190252 446532 | 84413 10026 380599 38.0 | 1.157 % | c | 10439 | 190252 446532 | 92854 10366 387470 37.4 | 1.157 % | c | 10945 | 190252 446532 | 102140 10872 406819 37.4 | 1.157 % | c ============================================================================== c [1mFound solution: 1326[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11585 | 190286 446619 | 63428 11512 555064 48.2 | 1.157 % | c | 11686 | 190286 446619 | 69770 11613 558245 48.1 | 1.158 % | c | 11839 | 190286 446619 | 76747 11766 566083 48.1 | 1.158 % | c | 12064 | 190286 446619 | 84422 11991 577304 48.1 | 1.158 % | c | 12402 | 190286 446619 | 92864 12329 581418 47.2 | 1.158 % | c | 12908 | 190258 446556 | 102151 12834 604153 47.1 | 1.167 % | c | 13667 | 190204 446436 | 112366 13589 636533 46.8 | 1.190 % | c | 14806 | 190153 446322 | 123603 14720 668941 45.4 | 1.212 % | c | 16514 | 189969 445907 | 135963 16409 754857 46.0 | 1.289 % | c | 19076 | 189969 445907 | 149559 18971 880480 46.4 | 1.289 % | c | 22921 | 189969 445907 | 164515 22816 1083581 47.5 | 1.289 % | c | 28688 | 189969 445907 | 180967 28583 1429962 50.0 | 1.289 % | c | 37340 | 189969 445907 | 199064 37235 2157656 57.9 | 1.289 % | c | 50318 | 189969 445907 | 218970 50213 4133473 82.3 | 1.289 % | c | 69780 | 189969 445907 | 240867 69675 7316398 105.0 | 1.289 % | c | 98972 | 189969 445907 | 264954 98867 9521248 96.3 | 1.289 % |
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/11662/stat): 11662 (minisat+_script) R 11661 11662 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843295459 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/11662/statm): 174 3 169 147 0 27 0 [pid=11662] 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=11663 New process pid=11664 New process pid=11665 execve syscall for /bin/sed executable One traced child (pid=11664) 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=11665) exited with status: 0 One traced child (pid=11663) exited with status: 0 New process pid=11666 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-cmb.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3594 0 0 0 968 14 0 0 25 0 1 0 1843295464 15970304 3368 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 3899 3368 145 145 0 3754 0 [pid=11666] vsize: 15596 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 17720 [startup+20.0061 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3720 0 0 0 1965 15 0 0 25 0 1 0 1843295464 16494592 3494 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 4027 3494 145 145 0 3882 0 [pid=11666] vsize: 16108 Current children cumulated CPU time (s) 19.81 Current children cumulated vsize (Kb) 18232 [startup+30.0069 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 3881 0 0 0 2962 17 0 0 25 0 1 0 1843295464 17154048 3655 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 4188 3655 145 145 0 4043 0 [pid=11666] vsize: 16752 Current children cumulated CPU time (s) 29.8 Current children cumulated vsize (Kb) 18876 [startup+40.0077 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6367 0 0 0 3942 27 0 0 25 0 1 0 1843295464 30191616 6099 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7371 6099 145 145 0 7226 0 [pid=11666] vsize: 29484 Current children cumulated CPU time (s) 39.7 Current children cumulated vsize (Kb) 31608 [startup+50.0095 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6675 0 0 0 4941 28 0 0 25 0 1 0 1843295464 30900224 6281 4294967295 134512640 135094434 3221224448 3221223072 134557619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7544 6281 145 145 0 7399 0 [pid=11666] vsize: 30176 Current children cumulated CPU time (s) 49.7 Current children cumulated vsize (Kb) 32300 [startup+60.0103 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6760 0 0 0 5939 29 0 0 25 0 1 0 1843295464 31248384 6366 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7629 6366 145 145 0 7484 0 [pid=11666] vsize: 30516 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 32640 [startup+70.0121 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 6953 0 0 0 6937 30 0 0 25 0 1 0 1843295464 31760384 6492 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7754 6492 145 145 0 7609 0 [pid=11666] vsize: 31016 Current children cumulated CPU time (s) 69.68 Current children cumulated vsize (Kb) 33140 [startup+80.0129 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7029 0 0 0 7935 31 0 0 25 0 1 0 1843295464 32063488 6568 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7828 6568 145 145 0 7683 0 [pid=11666] vsize: 31312 Current children cumulated CPU time (s) 79.67 Current children cumulated vsize (Kb) 33436 [startup+90.0127 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7086 0 0 0 8934 32 0 0 25 0 1 0 1843295464 32292864 6625 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7884 6625 145 145 0 7739 0 [pid=11666] vsize: 31536 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 33660 [startup+100.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7165 0 0 0 9933 33 0 0 25 0 1 0 1843295464 32677888 6704 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 7978 6704 145 145 0 7833 0 [pid=11666] vsize: 31912 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 34036 [startup+110.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7233 0 0 0 10932 33 0 0 25 0 1 0 1843295464 32948224 6772 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8044 6772 145 145 0 7899 0 [pid=11666] vsize: 32176 Current children cumulated CPU time (s) 109.66 Current children cumulated vsize (Kb) 34300 [startup+120.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7292 0 0 0 11931 34 0 0 25 0 1 0 1843295464 33185792 6831 4294967295 134512640 135094434 3221224448 3221223136 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8102 6831 145 145 0 7957 0 [pid=11666] vsize: 32408 Current children cumulated CPU time (s) 119.66 Current children cumulated vsize (Kb) 34532 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7346 0 0 0 12931 34 0 0 25 0 1 0 1843295464 33406976 6885 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8156 6885 145 145 0 8011 0 [pid=11666] vsize: 32624 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 34748 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7409 0 0 0 13930 35 0 0 25 0 1 0 1843295464 33660928 6948 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8218 6948 145 145 0 8073 0 [pid=11666] vsize: 32872 Current children cumulated CPU time (s) 139.66 Current children cumulated vsize (Kb) 34996 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7479 0 0 0 14928 35 0 0 25 0 1 0 1843295464 33943552 7018 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8287 7018 145 145 0 8142 0 [pid=11666] vsize: 33148 Current children cumulated CPU time (s) 149.64 Current children cumulated vsize (Kb) 35272 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7560 0 0 0 15927 36 0 0 25 0 1 0 1843295464 34267136 7099 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8366 7099 145 145 0 8221 0 [pid=11666] vsize: 33464 Current children cumulated CPU time (s) 159.64 Current children cumulated vsize (Kb) 35588 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7645 0 0 0 16926 37 0 0 25 0 1 0 1843295464 34611200 7184 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8450 7184 145 145 0 8305 0 [pid=11666] vsize: 33800 Current children cumulated CPU time (s) 169.64 Current children cumulated vsize (Kb) 35924 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7722 0 0 0 17925 37 0 0 25 0 1 0 1843295464 34922496 7261 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8526 7261 145 145 0 8381 0 [pid=11666] vsize: 34104 Current children cumulated CPU time (s) 179.63 Current children cumulated vsize (Kb) 36228 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7823 0 0 0 18923 38 0 0 25 0 1 0 1843295464 35332096 7362 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8626 7362 145 145 0 8481 0 [pid=11666] vsize: 34504 Current children cumulated CPU time (s) 189.62 Current children cumulated vsize (Kb) 36628 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 7933 0 0 0 19921 40 0 0 25 0 1 0 1843295464 35778560 7472 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8735 7472 145 145 0 8590 0 [pid=11666] vsize: 34940 Current children cumulated CPU time (s) 199.62 Current children cumulated vsize (Kb) 37064 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8009 0 0 0 20920 40 0 0 25 0 1 0 1843295464 36085760 7548 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8810 7548 145 145 0 8665 0 [pid=11666] vsize: 35240 Current children cumulated CPU time (s) 209.61 Current children cumulated vsize (Kb) 37364 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8082 0 0 0 21918 41 0 0 25 0 1 0 1843295464 36388864 7621 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8884 7621 145 145 0 8739 0 [pid=11666] vsize: 35536 Current children cumulated CPU time (s) 219.6 Current children cumulated vsize (Kb) 37660 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8166 0 0 0 22917 42 0 0 25 0 1 0 1843295464 36728832 7705 4294967295 134512640 135094434 3221224448 3221223040 134557208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 8967 7705 145 145 0 8822 0 [pid=11666] vsize: 35868 Current children cumulated CPU time (s) 229.6 Current children cumulated vsize (Kb) 37992 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8247 0 0 0 23915 43 0 0 25 0 1 0 1843295464 37056512 7786 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9047 7786 145 145 0 8902 0 [pid=11666] vsize: 36188 Current children cumulated CPU time (s) 239.59 Current children cumulated vsize (Kb) 38312 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8319 0 0 0 24915 43 0 0 25 0 1 0 1843295464 37351424 7858 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9119 7858 145 145 0 8974 0 [pid=11666] vsize: 36476 Current children cumulated CPU time (s) 249.59 Current children cumulated vsize (Kb) 38600 [startup+260.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8407 0 0 0 25914 44 0 0 25 0 1 0 1843295464 37838848 7946 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9238 7946 145 145 0 9093 0 [pid=11666] vsize: 36952 Current children cumulated CPU time (s) 259.59 Current children cumulated vsize (Kb) 39076 [startup+270.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8454 0 0 0 26913 44 0 0 25 0 1 0 1843295464 38031360 7993 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9285 7993 145 145 0 9140 0 [pid=11666] vsize: 37140 Current children cumulated CPU time (s) 269.58 Current children cumulated vsize (Kb) 39264 [startup+280.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8533 0 0 0 27912 45 0 0 25 0 1 0 1843295464 38350848 8072 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9363 8072 145 145 0 9218 0 [pid=11666] vsize: 37452 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 39576 [startup+290.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8602 0 0 0 28910 46 0 0 25 0 1 0 1843295464 38629376 8141 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9431 8141 145 145 0 9286 0 [pid=11666] vsize: 37724 Current children cumulated CPU time (s) 289.57 Current children cumulated vsize (Kb) 39848 [startup+300.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8661 0 0 0 29909 47 0 0 25 0 1 0 1843295464 38871040 8200 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9490 8200 145 145 0 9345 0 [pid=11666] vsize: 37960 Current children cumulated CPU time (s) 299.57 Current children cumulated vsize (Kb) 40084 [startup+310.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8731 0 0 0 30908 48 0 0 25 0 1 0 1843295464 39153664 8270 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9559 8270 145 145 0 9414 0 [pid=11666] vsize: 38236 Current children cumulated CPU time (s) 309.57 Current children cumulated vsize (Kb) 40360 [startup+320.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8794 0 0 0 31907 48 0 0 25 0 1 0 1843295464 39403520 8333 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9620 8333 145 145 0 9475 0 [pid=11666] vsize: 38480 Current children cumulated CPU time (s) 319.56 Current children cumulated vsize (Kb) 40604 [startup+330.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8866 0 0 0 32906 48 0 0 25 0 1 0 1843295464 39694336 8405 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9691 8405 145 145 0 9546 0 [pid=11666] vsize: 38764 Current children cumulated CPU time (s) 329.55 Current children cumulated vsize (Kb) 40888 [startup+340.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 8933 0 0 0 33904 49 0 0 25 0 1 0 1843295464 39964672 8472 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9757 8472 145 145 0 9612 0 [pid=11666] vsize: 39028 Current children cumulated CPU time (s) 339.54 Current children cumulated vsize (Kb) 41152 [startup+350.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9020 0 0 0 34903 50 0 0 25 0 1 0 1843295464 40316928 8559 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9843 8559 145 145 0 9698 0 [pid=11666] vsize: 39372 Current children cumulated CPU time (s) 349.54 Current children cumulated vsize (Kb) 41496 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9128 0 0 0 35901 51 0 0 25 0 1 0 1843295464 40755200 8667 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 9950 8667 145 145 0 9805 0 [pid=11666] vsize: 39800 Current children cumulated CPU time (s) 359.53 Current children cumulated vsize (Kb) 41924 [startup+370.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9239 0 0 0 36899 52 0 0 25 0 1 0 1843295464 41205760 8778 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10060 8778 145 145 0 9915 0 [pid=11666] vsize: 40240 Current children cumulated CPU time (s) 369.52 Current children cumulated vsize (Kb) 42364 [startup+380.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9330 0 0 0 37898 52 0 0 25 0 1 0 1843295464 41574400 8869 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10150 8869 145 145 0 10005 0 [pid=11666] vsize: 40600 Current children cumulated CPU time (s) 379.51 Current children cumulated vsize (Kb) 42724 [startup+390.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9470 0 0 0 38895 53 0 0 25 0 1 0 1843295464 42147840 9009 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10290 9009 145 145 0 10145 0 [pid=11666] vsize: 41160 Current children cumulated CPU time (s) 389.49 Current children cumulated vsize (Kb) 43284 [startup+400.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9624 0 0 0 39893 54 0 0 25 0 1 0 1843295464 42774528 9163 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10443 9163 145 145 0 10298 0 [pid=11666] vsize: 41772 Current children cumulated CPU time (s) 399.48 Current children cumulated vsize (Kb) 43896 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9775 0 0 0 40891 55 0 0 25 0 1 0 1843295464 43388928 9314 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10593 9314 145 145 0 10448 0 [pid=11666] vsize: 42372 Current children cumulated CPU time (s) 409.47 Current children cumulated vsize (Kb) 44496 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 9903 0 0 0 41889 57 0 0 25 0 1 0 1843295464 43913216 9442 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10721 9442 145 145 0 10576 0 [pid=11666] vsize: 42884 Current children cumulated CPU time (s) 419.47 Current children cumulated vsize (Kb) 45008 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10028 0 0 0 42887 57 0 0 25 0 1 0 1843295464 44421120 9567 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10845 9567 145 145 0 10700 0 [pid=11666] vsize: 43380 Current children cumulated CPU time (s) 429.45 Current children cumulated vsize (Kb) 45504 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10171 0 0 0 43885 58 0 0 25 0 1 0 1843295464 45002752 9710 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 10987 9710 145 145 0 10842 0 [pid=11666] vsize: 43948 Current children cumulated CPU time (s) 439.44 Current children cumulated vsize (Kb) 46072 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10332 0 0 0 44882 59 0 0 25 0 1 0 1843295464 45662208 9871 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11148 9871 145 145 0 11003 0 [pid=11666] vsize: 44592 Current children cumulated CPU time (s) 449.42 Current children cumulated vsize (Kb) 46716 [startup+460.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10480 0 0 0 45879 61 0 0 25 0 1 0 1843295464 46264320 10019 4294967295 134512640 135094434 3221224448 3221223040 134556933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11295 10019 145 145 0 11150 0 [pid=11666] vsize: 45180 Current children cumulated CPU time (s) 459.41 Current children cumulated vsize (Kb) 47304 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10654 0 0 0 46876 63 0 0 25 0 1 0 1843295464 46989312 10193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11472 10193 145 145 0 11327 0 [pid=11666] vsize: 45888 Current children cumulated CPU time (s) 469.4 Current children cumulated vsize (Kb) 48012 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10796 0 0 0 47874 64 0 0 25 0 1 0 1843295464 47562752 10335 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11612 10335 145 145 0 11467 0 [pid=11666] vsize: 46448 Current children cumulated CPU time (s) 479.39 Current children cumulated vsize (Kb) 48572 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 10929 0 0 0 48872 65 0 0 25 0 1 0 1843295464 48115712 10468 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11747 10468 145 145 0 11602 0 [pid=11666] vsize: 46988 Current children cumulated CPU time (s) 489.38 Current children cumulated vsize (Kb) 49112 [startup+500.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11029 0 0 0 49870 66 0 0 25 0 1 0 1843295464 48517120 10568 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11845 10568 145 145 0 11700 0 [pid=11666] vsize: 47380 Current children cumulated CPU time (s) 499.37 Current children cumulated vsize (Kb) 49504 [startup+510.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11118 0 0 0 50868 67 0 0 25 0 1 0 1843295464 48877568 10657 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 11933 10657 145 145 0 11788 0 [pid=11666] vsize: 47732 Current children cumulated CPU time (s) 509.36 Current children cumulated vsize (Kb) 49856 [startup+520.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11228 0 0 0 51866 68 0 0 25 0 1 0 1843295464 49324032 10767 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12042 10767 145 145 0 11897 0 [pid=11666] vsize: 48168 Current children cumulated CPU time (s) 519.35 Current children cumulated vsize (Kb) 50292 [startup+530.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11402 0 0 0 52864 70 0 0 19 0 1 0 1843295464 50032640 10941 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 12215 10941 145 145 0 12070 0 [pid=11666] vsize: 48860 Current children cumulated CPU time (s) 529.35 Current children cumulated vsize (Kb) 50984 [startup+540.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11525 0 0 0 53862 71 0 0 25 0 1 0 1843295464 50528256 11064 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12336 11064 145 145 0 12191 0 [pid=11666] vsize: 49344 Current children cumulated CPU time (s) 539.34 Current children cumulated vsize (Kb) 51468 [startup+550.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11615 0 0 0 54860 72 0 0 25 0 1 0 1843295464 50892800 11154 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12425 11154 145 145 0 12280 0 [pid=11666] vsize: 49700 Current children cumulated CPU time (s) 549.33 Current children cumulated vsize (Kb) 51824 [startup+560.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11715 0 0 0 55858 73 0 0 25 0 1 0 1843295464 51302400 11254 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12525 11254 145 145 0 12380 0 [pid=11666] vsize: 50100 Current children cumulated CPU time (s) 559.32 Current children cumulated vsize (Kb) 52224 [startup+570.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11846 0 0 0 56856 74 0 0 25 0 1 0 1843295464 51838976 11385 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12656 11385 145 145 0 12511 0 [pid=11666] vsize: 50624 Current children cumulated CPU time (s) 569.31 Current children cumulated vsize (Kb) 52748 [startup+580.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 11976 0 0 0 57854 75 0 0 25 0 1 0 1843295464 52363264 11515 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12784 11515 145 145 0 12639 0 [pid=11666] vsize: 51136 Current children cumulated CPU time (s) 579.3 Current children cumulated vsize (Kb) 53260 [startup+590.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12108 0 0 0 58853 76 0 0 25 0 1 0 1843295464 52899840 11647 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 12915 11647 145 145 0 12770 0 [pid=11666] vsize: 51660 Current children cumulated CPU time (s) 589.3 Current children cumulated vsize (Kb) 53784 [startup+600.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12249 0 0 0 59850 76 0 0 25 0 1 0 1843295464 53477376 11788 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13056 11788 145 145 0 12911 0 [pid=11666] vsize: 52224 Current children cumulated CPU time (s) 599.27 Current children cumulated vsize (Kb) 54348 [startup+610.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12405 0 0 0 60848 78 0 0 25 0 1 0 1843295464 54112256 11944 4294967295 134512640 135094434 3221224448 3221223040 134557133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13211 11944 145 145 0 13066 0 [pid=11666] vsize: 52844 Current children cumulated CPU time (s) 609.27 Current children cumulated vsize (Kb) 54968 [startup+620.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12543 0 0 0 61845 79 0 0 25 0 1 0 1843295464 54677504 12082 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13349 12082 145 145 0 13204 0 [pid=11666] vsize: 53396 Current children cumulated CPU time (s) 619.25 Current children cumulated vsize (Kb) 55520 [startup+630.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12704 0 0 0 62843 79 0 0 25 0 1 0 1843295464 55377920 12243 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13520 12243 145 145 0 13375 0 [pid=11666] vsize: 54080 Current children cumulated CPU time (s) 629.23 Current children cumulated vsize (Kb) 56204 [startup+640.05 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12841 0 0 0 63841 80 0 0 25 0 1 0 1843295464 55934976 12380 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13656 12380 145 145 0 13511 0 [pid=11666] vsize: 54624 Current children cumulated CPU time (s) 639.22 Current children cumulated vsize (Kb) 56748 [startup+650.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 12965 0 0 0 64840 81 0 0 25 0 1 0 1843295464 56438784 12504 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13779 12504 145 145 0 13634 0 [pid=11666] vsize: 55116 Current children cumulated CPU time (s) 649.22 Current children cumulated vsize (Kb) 57240 [startup+660.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13100 0 0 0 65837 82 0 0 25 0 1 0 1843295464 56995840 12639 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 13915 12639 145 145 0 13770 0 [pid=11666] vsize: 55660 Current children cumulated CPU time (s) 659.2 Current children cumulated vsize (Kb) 57784 [startup+670.053 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13284 0 0 0 66835 83 0 0 25 0 1 0 1843295464 57757696 12823 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 14101 12823 145 145 0 13956 0 [pid=11666] vsize: 56404 Current children cumulated CPU time (s) 669.19 Current children cumulated vsize (Kb) 58528 [startup+680.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13457 0 0 0 67832 85 0 0 25 0 1 0 1843295464 58728448 12996 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 14338 12996 145 145 0 14193 0 [pid=11666] vsize: 57352 Current children cumulated CPU time (s) 679.18 Current children cumulated vsize (Kb) 59476 [startup+690.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13609 0 0 0 68830 87 0 0 25 0 1 0 1843295464 59342848 13148 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 14488 13148 145 145 0 14343 0 [pid=11666] vsize: 57952 Current children cumulated CPU time (s) 689.18 Current children cumulated vsize (Kb) 60076 [startup+700.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13769 0 0 0 69828 88 0 0 25 0 1 0 1843295464 59990016 13308 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 14646 13308 145 145 0 14501 0 [pid=11666] vsize: 58584 Current children cumulated CPU time (s) 699.17 Current children cumulated vsize (Kb) 60708 [startup+710.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 13897 0 0 0 70824 89 0 0 25 0 1 0 1843295464 60510208 13436 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 14773 13436 145 145 0 14628 0 [pid=11666] vsize: 59092 Current children cumulated CPU time (s) 709.14 Current children cumulated vsize (Kb) 61216 [startup+720.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14052 0 0 0 71823 90 0 0 25 0 1 0 1843295464 61140992 13591 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 14927 13591 145 145 0 14782 0 [pid=11666] vsize: 59708 Current children cumulated CPU time (s) 719.14 Current children cumulated vsize (Kb) 61832 [startup+730.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14188 0 0 0 72820 91 0 0 25 0 1 0 1843295464 61698048 13727 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15063 13727 145 145 0 14918 0 [pid=11666] vsize: 60252 Current children cumulated CPU time (s) 729.12 Current children cumulated vsize (Kb) 62376 [startup+740.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14292 0 0 0 73817 92 0 0 25 0 1 0 1843295464 62140416 13831 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 15171 13831 145 145 0 15026 0 [pid=11666] vsize: 60684 Current children cumulated CPU time (s) 739.1 Current children cumulated vsize (Kb) 62808 [startup+750.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14343 0 0 0 74815 93 0 0 25 0 1 0 1843295464 62345216 13882 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 15221 13882 145 145 0 15076 0 [pid=11666] vsize: 60884 Current children cumulated CPU time (s) 749.09 Current children cumulated vsize (Kb) 63008 [startup+760.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14394 0 0 0 75814 94 0 0 25 0 1 0 1843295464 62554112 13933 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15272 13933 145 145 0 15127 0 [pid=11666] vsize: 61088 Current children cumulated CPU time (s) 759.09 Current children cumulated vsize (Kb) 63212 [startup+770.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14446 0 0 0 76813 94 0 0 25 0 1 0 1843295464 62763008 13985 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15323 13985 145 145 0 15178 0 [pid=11666] vsize: 61292 Current children cumulated CPU time (s) 769.08 Current children cumulated vsize (Kb) 63416 [startup+780.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14502 0 0 0 77813 94 0 0 25 0 1 0 1843295464 62988288 14041 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15378 14041 145 145 0 15233 0 [pid=11666] vsize: 61512 Current children cumulated CPU time (s) 779.08 Current children cumulated vsize (Kb) 63636 [startup+790.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14563 0 0 0 78811 95 0 0 25 0 1 0 1843295464 63238144 14102 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15439 14102 145 145 0 15294 0 [pid=11666] vsize: 61756 Current children cumulated CPU time (s) 789.07 Current children cumulated vsize (Kb) 63880 [startup+800.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14614 0 0 0 79811 95 0 0 25 0 1 0 1843295464 63451136 14153 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15491 14153 145 145 0 15346 0 [pid=11666] vsize: 61964 Current children cumulated CPU time (s) 799.07 Current children cumulated vsize (Kb) 64088 [startup+810.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14671 0 0 0 80810 96 0 0 25 0 1 0 1843295464 63680512 14210 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15547 14210 145 145 0 15402 0 [pid=11666] vsize: 62188 Current children cumulated CPU time (s) 809.07 Current children cumulated vsize (Kb) 64312 [startup+820.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14731 0 0 0 81809 96 0 0 25 0 1 0 1843295464 63926272 14270 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15607 14270 145 145 0 15462 0 [pid=11666] vsize: 62428 Current children cumulated CPU time (s) 819.06 Current children cumulated vsize (Kb) 64552 [startup+830.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14782 0 0 0 82808 97 0 0 25 0 1 0 1843295464 64135168 14321 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15658 14321 145 145 0 15513 0 [pid=11666] vsize: 62632 Current children cumulated CPU time (s) 829.06 Current children cumulated vsize (Kb) 64756 [startup+840.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14835 0 0 0 83808 97 0 0 25 0 1 0 1843295464 64348160 14374 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15710 14374 145 145 0 15565 0 [pid=11666] vsize: 62840 Current children cumulated CPU time (s) 839.06 Current children cumulated vsize (Kb) 64964 [startup+850.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14881 0 0 0 84807 97 0 0 25 0 1 0 1843295464 64536576 14420 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15756 14420 145 145 0 15611 0 [pid=11666] vsize: 63024 Current children cumulated CPU time (s) 849.05 Current children cumulated vsize (Kb) 65148 [startup+860.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 14955 0 0 0 85806 98 0 0 25 0 1 0 1843295464 64831488 14494 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15828 14494 145 145 0 15683 0 [pid=11666] vsize: 63312 Current children cumulated CPU time (s) 859.05 Current children cumulated vsize (Kb) 65436 [startup+870.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15014 0 0 0 86804 99 0 0 25 0 1 0 1843295464 65069056 14553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15886 14553 145 145 0 15741 0 [pid=11666] vsize: 63544 Current children cumulated CPU time (s) 869.04 Current children cumulated vsize (Kb) 65668 [startup+880.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15064 0 0 0 87804 99 0 0 25 0 1 0 1843295464 65273856 14603 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15936 14603 145 145 0 15791 0 [pid=11666] vsize: 63744 Current children cumulated CPU time (s) 879.04 Current children cumulated vsize (Kb) 65868 [startup+890.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15116 0 0 0 88803 99 0 0 25 0 1 0 1843295464 65482752 14655 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 15987 14655 145 145 0 15842 0 [pid=11666] vsize: 63948 Current children cumulated CPU time (s) 889.03 Current children cumulated vsize (Kb) 66072 [startup+900.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15171 0 0 0 89802 100 0 0 25 0 1 0 1843295464 65703936 14710 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16041 14710 145 145 0 15896 0 [pid=11666] vsize: 64164 Current children cumulated CPU time (s) 899.03 Current children cumulated vsize (Kb) 66288 [startup+910.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15222 0 0 0 90801 100 0 0 25 0 1 0 1843295464 65912832 14761 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16092 14761 145 145 0 15947 0 [pid=11666] vsize: 64368 Current children cumulated CPU time (s) 909.02 Current children cumulated vsize (Kb) 66492 [startup+920.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15268 0 0 0 91801 100 0 0 25 0 1 0 1843295464 66097152 14807 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16137 14807 145 145 0 15992 0 [pid=11666] vsize: 64548 Current children cumulated CPU time (s) 919.02 Current children cumulated vsize (Kb) 66672 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15318 0 0 0 92801 101 0 0 25 0 1 0 1843295464 66301952 14857 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16187 14857 145 145 0 16042 0 [pid=11666] vsize: 64748 Current children cumulated CPU time (s) 929.03 Current children cumulated vsize (Kb) 66872 [startup+940.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15359 0 0 0 93800 101 0 0 25 0 1 0 1843295464 66461696 14898 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16226 14898 145 145 0 16081 0 [pid=11666] vsize: 64904 Current children cumulated CPU time (s) 939.02 Current children cumulated vsize (Kb) 67028 [startup+950.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15405 0 0 0 94800 101 0 0 25 0 1 0 1843295464 66646016 14944 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16271 14944 145 145 0 16126 0 [pid=11666] vsize: 65084 Current children cumulated CPU time (s) 949.02 Current children cumulated vsize (Kb) 67208 [startup+960.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15446 0 0 0 95799 101 0 0 25 0 1 0 1843295464 66818048 14985 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16313 14985 145 145 0 16168 0 [pid=11666] vsize: 65252 Current children cumulated CPU time (s) 959.01 Current children cumulated vsize (Kb) 67376 [startup+970.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15521 0 0 0 96798 102 0 0 25 0 1 0 1843295464 67121152 15060 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16387 15060 145 145 0 16242 0 [pid=11666] vsize: 65548 Current children cumulated CPU time (s) 969.01 Current children cumulated vsize (Kb) 67672 [startup+980.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15577 0 0 0 97798 102 0 0 25 0 1 0 1843295464 67350528 15116 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16443 15116 145 145 0 16298 0 [pid=11666] vsize: 65772 Current children cumulated CPU time (s) 979.01 Current children cumulated vsize (Kb) 67896 [startup+990.076 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15627 0 0 0 98797 103 0 0 25 0 1 0 1843295464 67551232 15166 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16492 15166 145 145 0 16347 0 [pid=11666] vsize: 65968 Current children cumulated CPU time (s) 989.01 Current children cumulated vsize (Kb) 68092 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15682 0 0 0 99796 103 0 0 25 0 1 0 1843295464 67772416 15221 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16546 15221 145 145 0 16401 0 [pid=11666] vsize: 66184 Current children cumulated CPU time (s) 999 Current children cumulated vsize (Kb) 68308 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15739 0 0 0 100795 103 0 0 25 0 1 0 1843295464 68001792 15278 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16602 15278 145 145 0 16457 0 [pid=11666] vsize: 66408 Current children cumulated CPU time (s) 1008.99 Current children cumulated vsize (Kb) 68532 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15800 0 0 0 101794 104 0 0 25 0 1 0 1843295464 68247552 15339 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16662 15339 145 145 0 16517 0 [pid=11666] vsize: 66648 Current children cumulated CPU time (s) 1018.99 Current children cumulated vsize (Kb) 68772 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15864 0 0 0 102792 105 0 0 25 0 1 0 1843295464 68509696 15403 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16726 15403 145 145 0 16581 0 [pid=11666] vsize: 66904 Current children cumulated CPU time (s) 1028.98 Current children cumulated vsize (Kb) 69028 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15925 0 0 0 103791 105 0 0 25 0 1 0 1843295464 68759552 15464 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16787 15464 145 145 0 16642 0 [pid=11666] vsize: 67148 Current children cumulated CPU time (s) 1038.97 Current children cumulated vsize (Kb) 69272 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 15997 0 0 0 104790 106 0 0 25 0 1 0 1843295464 69050368 15536 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16858 15536 145 145 0 16713 0 [pid=11666] vsize: 67432 Current children cumulated CPU time (s) 1048.97 Current children cumulated vsize (Kb) 69556 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16077 0 0 0 105788 107 0 0 25 0 1 0 1843295464 69373952 15616 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16937 15616 145 145 0 16792 0 [pid=11666] vsize: 67748 Current children cumulated CPU time (s) 1058.96 Current children cumulated vsize (Kb) 69872 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16138 0 0 0 106787 108 0 0 25 0 1 0 1843295464 69623808 15677 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 16998 15677 145 145 0 16853 0 [pid=11666] vsize: 67992 Current children cumulated CPU time (s) 1068.96 Current children cumulated vsize (Kb) 70116 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16195 0 0 0 107787 108 0 0 25 0 1 0 1843295464 69853184 15734 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 17054 15734 145 145 0 16909 0 [pid=11666] vsize: 68216 Current children cumulated CPU time (s) 1078.96 Current children cumulated vsize (Kb) 70340 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16261 0 0 0 108787 108 0 0 25 0 1 0 1843295464 70131712 15800 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11666/statm): 17122 15800 145 145 0 16977 0 [pid=11666] vsize: 68488 Current children cumulated CPU time (s) 1088.96 Current children cumulated vsize (Kb) 70612 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16326 0 0 0 109786 109 0 0 25 0 1 0 1843295464 70393856 15865 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17186 15865 145 145 0 17041 0 [pid=11666] vsize: 68744 Current children cumulated CPU time (s) 1098.96 Current children cumulated vsize (Kb) 70868 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16380 0 0 0 110785 109 0 0 25 0 1 0 1843295464 70615040 15919 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17240 15919 145 145 0 17095 0 [pid=11666] vsize: 68960 Current children cumulated CPU time (s) 1108.95 Current children cumulated vsize (Kb) 71084 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16444 0 0 0 111783 110 0 0 25 0 1 0 1843295464 70868992 15983 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17302 15983 145 145 0 17157 0 [pid=11666] vsize: 69208 Current children cumulated CPU time (s) 1118.94 Current children cumulated vsize (Kb) 71332 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16498 0 0 0 112782 111 0 0 25 0 1 0 1843295464 71081984 16037 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17354 16037 145 145 0 17209 0 [pid=11666] vsize: 69416 Current children cumulated CPU time (s) 1128.94 Current children cumulated vsize (Kb) 71540 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16554 0 0 0 113781 112 0 0 25 0 1 0 1843295464 71311360 16093 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17410 16093 145 145 0 17265 0 [pid=11666] vsize: 69640 Current children cumulated CPU time (s) 1138.94 Current children cumulated vsize (Kb) 71764 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16611 0 0 0 114779 113 0 0 25 0 1 0 1843295464 71544832 16150 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17467 16150 145 145 0 17322 0 [pid=11666] vsize: 69868 Current children cumulated CPU time (s) 1148.93 Current children cumulated vsize (Kb) 71992 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16662 0 0 0 115778 114 0 0 25 0 1 0 1843295464 71753728 16201 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17518 16201 145 145 0 17373 0 [pid=11666] vsize: 70072 Current children cumulated CPU time (s) 1158.93 Current children cumulated vsize (Kb) 72196 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16715 0 0 0 116776 115 0 0 25 0 1 0 1843295464 71966720 16254 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17570 16254 145 145 0 17425 0 [pid=11666] vsize: 70280 Current children cumulated CPU time (s) 1168.92 Current children cumulated vsize (Kb) 72404 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16780 0 0 0 117775 115 0 0 25 0 1 0 1843295464 72249344 16319 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17639 16319 145 145 0 17494 0 [pid=11666] vsize: 70556 Current children cumulated CPU time (s) 1178.91 Current children cumulated vsize (Kb) 72680 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16832 0 0 0 118774 116 0 0 25 0 1 0 1843295464 72454144 16371 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17689 16371 145 145 0 17544 0 [pid=11666] vsize: 70756 Current children cumulated CPU time (s) 1188.91 Current children cumulated vsize (Kb) 72880 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16882 0 0 0 119774 116 0 0 25 0 1 0 1843295464 72663040 16421 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17740 16421 145 145 0 17595 0 [pid=11666] vsize: 70960 Current children cumulated CPU time (s) 1198.91 Current children cumulated vsize (Kb) 73084 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16942 0 0 0 120772 117 0 0 25 0 1 0 1843295464 72904704 16481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17799 16481 145 145 0 17654 0 [pid=11666] vsize: 71196 Current children cumulated CPU time (s) 1208.9 Current children cumulated vsize (Kb) 73320 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 11666 Raw data (/proc/11662/stat): 11662 (minisat+_script) S 11661 11662 5929 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843295459 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11662/statm): 531 226 485 147 0 384 0 [pid=11662] vsize: 2124 Raw data (/proc/11666/stat): 11666 (minisat+_64-bit) R 11662 11662 5929 0 -1 0 16942 0 0 0 120772 117 0 0 25 0 1 0 1843295464 72904704 16481 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11666/statm): 17799 16481 145 145 0 17654 0 [pid=11666] vsize: 71196 Current children cumulated CPU time (s) 1208.9 Current children cumulated vsize (Kb) 73320 Sending SIGTERM to -11662 Sleeping 2 seconds One traced child (pid=11662) ended because it received signal 15 (SIGTERM) One traced child (pid=11666) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.94 CPU user time (s): 1207.73 CPU system time (s): 1.20782 CPU usage (%): 99.901 Max. virtual memory (cumulated for all children) (Kb): 73320
ERROR: no interpretation found !