Name | submitted/manquinho/logic-synthesis/normalized-5xp1.b.opb |
MD5SUM | 24a8f38e94b07e6ca192a34c96c24c6e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 12 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 465 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 465 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 465 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 73.2229 |
Number of variables | 464 |
Total number of constraints | 859 |
Number of constraints which are clauses | 845 |
Number of constraints which are cardinality constraints (but not clauses) | 14 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 149 |
LAUNCH ON wulflinc20 THE 2005-09-18 12:43:11 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2402 boxname=wulflinc20 idbench=58 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 24a8f38e94b07e6ca192a34c96c24c6e /oldhome/oroussel/tmp/wulflinc20/normalized-5xp1.b.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-5xp1.b.opb IDLAUNCH: 2402 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 938368 kB Buffers: 34596 kB Cached: 32980 kB SwapCached: 832 kB Active: 55072 kB Inactive: 15156 kB HighTotal: 131008 kB HighFree: 94332 kB LowTotal: 903652 kB LowFree: 844036 kB SwapTotal: 2097892 kB SwapFree: 2096604 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20500 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 13:03:21 (client local time) WITH STATUS 10 IN 1209.75 SECONDS stats: 2402 7 1209.75 10
c Parsing PB file... c Converting 843 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 | 843 29887 | 281 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 20[0m c ---[ 0]---> Sorter-cost:17506 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19368 73043 | 6456 0 0 nan | 0.000 % | c | 102 | 19368 73043 | 7101 102 7508 73.6 | 0.016 % | c | 253 | 19356 73019 | 7811 251 21282 84.8 | 0.056 % | c ============================================================================== c [1mFound solution: 17[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 293 | 17268 68155 | 5756 287 23635 82.4 | 0.056 % | c | 393 | 17268 68155 | 6331 387 30443 78.7 | 11.325 % | c | 543 | 17268 68155 | 6964 537 39041 72.7 | 11.325 % | c | 770 | 17268 68155 | 7661 764 50110 65.6 | 11.325 % | c ============================================================================== c [1mFound solution: 15[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 864 | 17261 68142 | 5753 845 54108 64.0 | 11.325 % | c | 964 | 17261 68142 | 6328 945 61405 65.0 | 11.470 % | c | 1115 | 17261 68142 | 6961 1096 75538 68.9 | 11.470 % | c | 1341 | 17261 68142 | 7657 1322 87753 66.4 | 11.470 % | c | 1678 | 17261 68142 | 8422 1659 110793 66.8 | 11.470 % | c | 2184 | 17261 68142 | 9265 2165 155258 71.7 | 11.470 % | c | 2943 | 17261 68142 | 10191 2924 219586 75.1 | 11.470 % | c ============================================================================== c [1mFound solution: 14[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3979 | 17273 68172 | 5757 3960 368681 93.1 | 11.470 % | c | 4081 | 17273 68172 | 6332 4062 376314 92.6 | 11.470 % | c | 4232 | 17273 68172 | 6965 4213 386712 91.8 | 11.470 % | c | 4457 | 17273 68172 | 7662 4438 409455 92.3 | 11.470 % | c | 4795 | 17273 68172 | 8428 4776 432918 90.6 | 11.470 % | c | 5301 | 17273 68172 | 9271 5282 466487 88.3 | 11.470 % | c | 6061 | 17273 68172 | 10198 6042 522550 86.5 | 11.470 % | c | 7204 | 17273 68172 | 11218 7185 589528 82.0 | 11.470 % | c | 8917 | 17273 68172 | 12340 8898 698521 78.5 | 11.470 % | c | 11480 | 17273 68172 | 13574 11461 858013 74.9 | 11.470 % | c | 15325 | 17273 68172 | 14932 15306 1141586 74.6 | 11.470 % | c | 21092 | 17273 68172 | 16425 12759 938327 73.5 | 11.470 % | c | 29741 | 17273 68172 | 18067 12053 875185 72.6 | 11.470 % | c | 42716 | 17273 68172 | 19874 14184 867021 61.1 | 11.470 % | c | 62178 | 17273 68172 | 21862 11498 890576 77.5 | 11.470 % | c | 91371 | 17273 68172 | 24048 15677 1206811 77.0 | 11.470 % | c | 135161 | 17273 68172 | 26453 20827 1226051 58.9 | 11.470 % | c | 200848 | 17273 68172 | 29098 27816 1466699 52.7 | 11.470 % | c | 299376 | 17273 68172 | 32008 25897 1765102 68.2 | 11.470 % |
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/6400/stat): 6400 (minisat+_script) R 6399 6400 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841344529 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/6400/statm): 174 3 169 147 0 27 0 [pid=6400] 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=6401 New process pid=6402 New process pid=6403 execve syscall for /bin/sed executable One traced child (pid=6402) 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=6403) exited with status: 0 One traced child (pid=6401) exited with status: 0 New process pid=6404 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-5xp1.b.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.95 0.90 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 1790 0 0 0 977 9 0 0 25 0 1 0 1841344534 7958528 1774 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 1943 1774 145 145 0 1798 0 [pid=6404] vsize: 7772 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 9896 [startup+20.005 s] Raw data (loadavg): 0.94 0.95 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2103 0 0 0 1970 12 0 0 25 0 1 0 1841344534 9256960 2087 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 2260 2087 145 145 0 2115 0 [pid=6404] vsize: 9040 Current children cumulated CPU time (s) 19.82 Current children cumulated vsize (Kb) 11164 [startup+30.0057 s] Raw data (loadavg): 0.95 0.95 0.91 1/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) T 6400 6400 2660 0 -1 0 2458 0 0 0 2964 15 0 0 25 0 1 0 1841344534 10698752 2442 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6404/statm): 2612 2442 145 145 0 2467 0 [pid=6404] vsize: 10448 Current children cumulated CPU time (s) 29.79 Current children cumulated vsize (Kb) 12572 [startup+40.0065 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2652 0 0 0 3960 16 0 0 25 0 1 0 1841344534 11563008 2636 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 2823 2636 145 145 0 2678 0 [pid=6404] vsize: 11292 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 13416 [startup+50.0082 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2652 0 0 0 4960 16 0 0 25 0 1 0 1841344534 11563008 2636 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 2823 2636 145 145 0 2678 0 [pid=6404] vsize: 11292 Current children cumulated CPU time (s) 49.76 Current children cumulated vsize (Kb) 13416 [startup+60.0089 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2664 0 0 0 5960 16 0 0 25 0 1 0 1841344534 11608064 2648 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 2834 2648 145 145 0 2689 0 [pid=6404] vsize: 11336 Current children cumulated CPU time (s) 59.76 Current children cumulated vsize (Kb) 13460 [startup+70.0106 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2855 0 0 0 6958 17 0 0 25 0 1 0 1841344534 12410880 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3030 2839 145 145 0 2885 0 [pid=6404] vsize: 12120 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 14244 [startup+80.0114 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2855 0 0 0 7958 17 0 0 25 0 1 0 1841344534 12410880 2839 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3030 2839 145 145 0 2885 0 [pid=6404] vsize: 12120 Current children cumulated CPU time (s) 79.75 Current children cumulated vsize (Kb) 14244 [startup+90.0121 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 2961 0 0 0 8956 18 0 0 25 0 1 0 1841344534 12849152 2945 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3137 2945 145 145 0 2992 0 [pid=6404] vsize: 12548 Current children cumulated CPU time (s) 89.74 Current children cumulated vsize (Kb) 14672 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3079 0 0 0 9954 19 0 0 25 0 1 0 1841344534 13332480 3063 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3255 3063 145 145 0 3110 0 [pid=6404] vsize: 13020 Current children cumulated CPU time (s) 99.73 Current children cumulated vsize (Kb) 15144 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3085 0 0 0 10954 19 0 0 25 0 1 0 1841344534 13365248 3069 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3263 3069 145 145 0 3118 0 [pid=6404] vsize: 13052 Current children cumulated CPU time (s) 109.73 Current children cumulated vsize (Kb) 15176 [startup+120.014 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3133 0 0 0 11954 19 0 0 25 0 1 0 1841344534 13574144 3117 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 3314 3117 145 145 0 3169 0 [pid=6404] vsize: 13256 Current children cumulated CPU time (s) 119.73 Current children cumulated vsize (Kb) 15380 [startup+130.015 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3338 0 0 0 12949 21 0 0 25 0 1 0 1841344534 14413824 3322 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3519 3322 145 145 0 3374 0 [pid=6404] vsize: 14076 Current children cumulated CPU time (s) 129.7 Current children cumulated vsize (Kb) 16200 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3356 0 0 0 13948 22 0 0 25 0 1 0 1841344534 14495744 3340 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3539 3340 145 145 0 3394 0 [pid=6404] vsize: 14156 Current children cumulated CPU time (s) 139.7 Current children cumulated vsize (Kb) 16280 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3396 0 0 0 14947 23 0 0 25 0 1 0 1841344534 14671872 3380 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3582 3380 145 145 0 3437 0 [pid=6404] vsize: 14328 Current children cumulated CPU time (s) 149.7 Current children cumulated vsize (Kb) 16452 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3638 0 0 0 15943 25 0 0 25 0 1 0 1841344534 15663104 3622 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3824 3622 145 145 0 3679 0 [pid=6404] vsize: 15296 Current children cumulated CPU time (s) 159.68 Current children cumulated vsize (Kb) 17420 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3671 0 0 0 16943 26 0 0 25 0 1 0 1841344534 15826944 3655 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3864 3655 145 145 0 3719 0 [pid=6404] vsize: 15456 Current children cumulated CPU time (s) 169.69 Current children cumulated vsize (Kb) 17580 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3684 0 0 0 17942 26 0 0 25 0 1 0 1841344534 15876096 3668 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3876 3668 145 145 0 3731 0 [pid=6404] vsize: 15504 Current children cumulated CPU time (s) 179.68 Current children cumulated vsize (Kb) 17628 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3729 0 0 0 18941 27 0 0 25 0 1 0 1841344534 16121856 3713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 3936 3713 145 145 0 3791 0 [pid=6404] vsize: 15744 Current children cumulated CPU time (s) 189.68 Current children cumulated vsize (Kb) 17868 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3773 0 0 0 19941 27 0 0 25 0 1 0 1841344534 16400384 3757 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4004 3757 145 145 0 3859 0 [pid=6404] vsize: 16016 Current children cumulated CPU time (s) 199.68 Current children cumulated vsize (Kb) 18140 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3774 0 0 0 20940 28 0 0 25 0 1 0 1841344534 16400384 3758 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4004 3758 145 145 0 3859 0 [pid=6404] vsize: 16016 Current children cumulated CPU time (s) 209.68 Current children cumulated vsize (Kb) 18140 [startup+220.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3786 0 0 0 21940 28 0 0 25 0 1 0 1841344534 16465920 3770 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4020 3770 145 145 0 3875 0 [pid=6404] vsize: 16080 Current children cumulated CPU time (s) 219.68 Current children cumulated vsize (Kb) 18204 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3786 0 0 0 22940 29 0 0 25 0 1 0 1841344534 16465920 3770 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4020 3770 145 145 0 3875 0 [pid=6404] vsize: 16080 Current children cumulated CPU time (s) 229.69 Current children cumulated vsize (Kb) 18204 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3798 0 0 0 23940 29 0 0 25 0 1 0 1841344534 16531456 3782 4294967295 134512640 135094434 3221224448 3221223040 134557334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4036 3782 145 145 0 3891 0 [pid=6404] vsize: 16144 Current children cumulated CPU time (s) 239.69 Current children cumulated vsize (Kb) 18268 [startup+250.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3893 0 0 0 24938 30 0 0 25 0 1 0 1841344534 16904192 3877 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4127 3877 145 145 0 3982 0 [pid=6404] vsize: 16508 Current children cumulated CPU time (s) 249.68 Current children cumulated vsize (Kb) 18632 [startup+260.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3985 0 0 0 25936 31 0 0 25 0 1 0 1841344534 17317888 3969 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4228 3969 145 145 0 4083 0 [pid=6404] vsize: 16912 Current children cumulated CPU time (s) 259.67 Current children cumulated vsize (Kb) 19036 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 3996 0 0 0 26936 31 0 0 25 0 1 0 1841344534 17416192 3980 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4252 3980 145 145 0 4107 0 [pid=6404] vsize: 17008 Current children cumulated CPU time (s) 269.67 Current children cumulated vsize (Kb) 19132 [startup+280.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4008 0 0 0 27936 32 0 0 25 0 1 0 1841344534 17481728 3992 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4268 3992 145 145 0 4123 0 [pid=6404] vsize: 17072 Current children cumulated CPU time (s) 279.68 Current children cumulated vsize (Kb) 19196 [startup+290.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4020 0 0 0 28935 32 0 0 25 0 1 0 1841344534 17547264 4004 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4284 4004 145 145 0 4139 0 [pid=6404] vsize: 17136 Current children cumulated CPU time (s) 289.67 Current children cumulated vsize (Kb) 19260 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4034 0 0 0 29935 33 0 0 25 0 1 0 1841344534 17612800 4018 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4300 4018 145 145 0 4155 0 [pid=6404] vsize: 17200 Current children cumulated CPU time (s) 299.68 Current children cumulated vsize (Kb) 19324 [startup+310.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4034 0 0 0 30935 33 0 0 25 0 1 0 1841344534 17612800 4018 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4300 4018 145 145 0 4155 0 [pid=6404] vsize: 17200 Current children cumulated CPU time (s) 309.68 Current children cumulated vsize (Kb) 19324 [startup+320.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4047 0 0 0 31935 33 0 0 25 0 1 0 1841344534 17645568 4031 4294967295 134512640 135094434 3221224448 3221223120 134555429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4308 4031 145 145 0 4163 0 [pid=6404] vsize: 17232 Current children cumulated CPU time (s) 319.68 Current children cumulated vsize (Kb) 19356 [startup+330.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4054 0 0 0 32934 34 0 0 25 0 1 0 1841344534 17694720 4038 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4320 4038 145 145 0 4175 0 [pid=6404] vsize: 17280 Current children cumulated CPU time (s) 329.68 Current children cumulated vsize (Kb) 19404 [startup+340.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4085 0 0 0 33934 34 0 0 25 0 1 0 1841344534 17842176 4069 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4356 4069 145 145 0 4211 0 [pid=6404] vsize: 17424 Current children cumulated CPU time (s) 339.68 Current children cumulated vsize (Kb) 19548 [startup+350.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4094 0 0 0 34933 35 0 0 25 0 1 0 1841344534 17874944 4078 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4364 4078 145 145 0 4219 0 [pid=6404] vsize: 17456 Current children cumulated CPU time (s) 349.68 Current children cumulated vsize (Kb) 19580 [startup+360.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4102 0 0 0 35933 35 0 0 25 0 1 0 1841344534 17907712 4086 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4372 4086 145 145 0 4227 0 [pid=6404] vsize: 17488 Current children cumulated CPU time (s) 359.68 Current children cumulated vsize (Kb) 19612 [startup+370.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4110 0 0 0 36933 36 0 0 25 0 1 0 1841344534 17940480 4094 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4380 4094 145 145 0 4235 0 [pid=6404] vsize: 17520 Current children cumulated CPU time (s) 369.69 Current children cumulated vsize (Kb) 19644 [startup+380.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4111 0 0 0 37932 36 0 0 25 0 1 0 1841344534 17940480 4095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4380 4095 145 145 0 4235 0 [pid=6404] vsize: 17520 Current children cumulated CPU time (s) 379.68 Current children cumulated vsize (Kb) 19644 [startup+390.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4114 0 0 0 38932 37 0 0 25 0 1 0 1841344534 17940480 4098 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4380 4098 145 145 0 4235 0 [pid=6404] vsize: 17520 Current children cumulated CPU time (s) 389.69 Current children cumulated vsize (Kb) 19644 [startup+400.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4114 0 0 0 39932 37 0 0 25 0 1 0 1841344534 17940480 4098 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4380 4098 145 145 0 4235 0 [pid=6404] vsize: 17520 Current children cumulated CPU time (s) 399.69 Current children cumulated vsize (Kb) 19644 [startup+410.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4121 0 0 0 40932 37 0 0 25 0 1 0 1841344534 17973248 4105 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4388 4105 145 145 0 4243 0 [pid=6404] vsize: 17552 Current children cumulated CPU time (s) 409.69 Current children cumulated vsize (Kb) 19676 [startup+420.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4131 0 0 0 41932 37 0 0 25 0 1 0 1841344534 18071552 4115 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4412 4115 145 145 0 4267 0 [pid=6404] vsize: 17648 Current children cumulated CPU time (s) 419.69 Current children cumulated vsize (Kb) 19772 [startup+430.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4132 0 0 0 42932 38 0 0 25 0 1 0 1841344534 18071552 4116 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4412 4116 145 145 0 4267 0 [pid=6404] vsize: 17648 Current children cumulated CPU time (s) 429.7 Current children cumulated vsize (Kb) 19772 [startup+440.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4138 0 0 0 43932 38 0 0 25 0 1 0 1841344534 18071552 4122 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4412 4122 145 145 0 4267 0 [pid=6404] vsize: 17648 Current children cumulated CPU time (s) 439.7 Current children cumulated vsize (Kb) 19772 [startup+450.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4138 0 0 0 44932 38 0 0 25 0 1 0 1841344534 18071552 4122 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4412 4122 145 145 0 4267 0 [pid=6404] vsize: 17648 Current children cumulated CPU time (s) 449.7 Current children cumulated vsize (Kb) 19772 [startup+460.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4146 0 0 0 45932 38 0 0 25 0 1 0 1841344534 18104320 4130 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4420 4130 145 145 0 4275 0 [pid=6404] vsize: 17680 Current children cumulated CPU time (s) 459.7 Current children cumulated vsize (Kb) 19804 [startup+470.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4157 0 0 0 46932 38 0 0 25 0 1 0 1841344534 18202624 4141 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4444 4141 145 145 0 4299 0 [pid=6404] vsize: 17776 Current children cumulated CPU time (s) 469.7 Current children cumulated vsize (Kb) 19900 [startup+480.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4158 0 0 0 47933 38 0 0 25 0 1 0 1841344534 18202624 4142 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4444 4142 145 145 0 4299 0 [pid=6404] vsize: 17776 Current children cumulated CPU time (s) 479.71 Current children cumulated vsize (Kb) 19900 [startup+490.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4158 0 0 0 48933 38 0 0 25 0 1 0 1841344534 18202624 4142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4444 4142 145 145 0 4299 0 [pid=6404] vsize: 17776 Current children cumulated CPU time (s) 489.71 Current children cumulated vsize (Kb) 19900 [startup+500.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4169 0 0 0 49933 38 0 0 25 0 1 0 1841344534 18235392 4153 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4452 4153 145 145 0 4307 0 [pid=6404] vsize: 17808 Current children cumulated CPU time (s) 499.71 Current children cumulated vsize (Kb) 19932 [startup+510.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4181 0 0 0 50933 38 0 0 25 0 1 0 1841344534 18300928 4165 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4468 4165 145 145 0 4323 0 [pid=6404] vsize: 17872 Current children cumulated CPU time (s) 509.71 Current children cumulated vsize (Kb) 19996 [startup+520.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4192 0 0 0 51934 38 0 0 25 0 1 0 1841344534 18366464 4176 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4484 4176 145 145 0 4339 0 [pid=6404] vsize: 17936 Current children cumulated CPU time (s) 519.72 Current children cumulated vsize (Kb) 20060 [startup+530.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4216 0 0 0 52934 38 0 0 25 0 1 0 1841344534 18497536 4200 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4516 4200 145 145 0 4371 0 [pid=6404] vsize: 18064 Current children cumulated CPU time (s) 529.72 Current children cumulated vsize (Kb) 20188 [startup+540.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4218 0 0 0 53934 38 0 0 25 0 1 0 1841344534 18497536 4202 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4516 4202 145 145 0 4371 0 [pid=6404] vsize: 18064 Current children cumulated CPU time (s) 539.72 Current children cumulated vsize (Kb) 20188 [startup+550.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 54934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0 [pid=6404] vsize: 18224 Current children cumulated CPU time (s) 549.72 Current children cumulated vsize (Kb) 20348 [startup+560.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 55934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0 [pid=6404] vsize: 18224 Current children cumulated CPU time (s) 559.72 Current children cumulated vsize (Kb) 20348 [startup+570.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4248 0 0 0 56934 38 0 0 25 0 1 0 1841344534 18661376 4232 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4556 4232 145 145 0 4411 0 [pid=6404] vsize: 18224 Current children cumulated CPU time (s) 569.72 Current children cumulated vsize (Kb) 20348 [startup+580.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4258 0 0 0 57934 38 0 0 25 0 1 0 1841344534 18726912 4242 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4572 4242 145 145 0 4427 0 [pid=6404] vsize: 18288 Current children cumulated CPU time (s) 579.72 Current children cumulated vsize (Kb) 20412 [startup+590.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4269 0 0 0 58935 38 0 0 25 0 1 0 1841344534 18792448 4253 4294967295 134512640 135094434 3221224448 3221223072 134557593 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6404/statm): 4588 4253 145 145 0 4443 0 [pid=6404] vsize: 18352 Current children cumulated CPU time (s) 589.73 Current children cumulated vsize (Kb) 20476 [startup+600.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4295 0 0 0 59934 39 0 0 25 0 1 0 1841344534 18923520 4279 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4620 4279 145 145 0 4475 0 [pid=6404] vsize: 18480 Current children cumulated CPU time (s) 599.73 Current children cumulated vsize (Kb) 20604 [startup+610.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 60934 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0 [pid=6404] vsize: 18480 Current children cumulated CPU time (s) 609.73 Current children cumulated vsize (Kb) 20604 [startup+620.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 61935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0 [pid=6404] vsize: 18480 Current children cumulated CPU time (s) 619.74 Current children cumulated vsize (Kb) 20604 [startup+630.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 62935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0 [pid=6404] vsize: 18480 Current children cumulated CPU time (s) 629.74 Current children cumulated vsize (Kb) 20604 [startup+640.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4296 0 0 0 63935 39 0 0 25 0 1 0 1841344534 18923520 4280 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4620 4280 145 145 0 4475 0 [pid=6404] vsize: 18480 Current children cumulated CPU time (s) 639.74 Current children cumulated vsize (Kb) 20604 [startup+650.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4313 0 0 0 64935 39 0 0 25 0 1 0 1841344534 19021824 4297 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4644 4297 145 145 0 4499 0 [pid=6404] vsize: 18576 Current children cumulated CPU time (s) 649.74 Current children cumulated vsize (Kb) 20700 [startup+660.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4317 0 0 0 65935 39 0 0 25 0 1 0 1841344534 19087360 4301 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4660 4301 145 145 0 4515 0 [pid=6404] vsize: 18640 Current children cumulated CPU time (s) 659.74 Current children cumulated vsize (Kb) 20764 [startup+670.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4317 0 0 0 66936 39 0 0 25 0 1 0 1841344534 19087360 4301 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4660 4301 145 145 0 4515 0 [pid=6404] vsize: 18640 Current children cumulated CPU time (s) 669.75 Current children cumulated vsize (Kb) 20764 [startup+680.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4328 0 0 0 67936 39 0 0 25 0 1 0 1841344534 19120128 4312 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4668 4312 145 145 0 4523 0 [pid=6404] vsize: 18672 Current children cumulated CPU time (s) 679.75 Current children cumulated vsize (Kb) 20796 [startup+690.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4338 0 0 0 68936 39 0 0 25 0 1 0 1841344534 19185664 4322 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4322 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 689.75 Current children cumulated vsize (Kb) 20860 [startup+700.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 69936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 699.75 Current children cumulated vsize (Kb) 20860 [startup+710.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 70936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 709.75 Current children cumulated vsize (Kb) 20860 [startup+720.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 71936 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 719.75 Current children cumulated vsize (Kb) 20860 [startup+730.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 72937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 729.76 Current children cumulated vsize (Kb) 20860 [startup+740.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 73937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 739.76 Current children cumulated vsize (Kb) 20860 [startup+750.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4340 0 0 0 74937 39 0 0 25 0 1 0 1841344534 19185664 4324 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4684 4324 145 145 0 4539 0 [pid=6404] vsize: 18736 Current children cumulated CPU time (s) 749.76 Current children cumulated vsize (Kb) 20860 [startup+760.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4526 0 0 0 75934 40 0 0 25 0 1 0 1841344534 19976192 4510 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 4877 4510 145 145 0 4732 0 [pid=6404] vsize: 19508 Current children cumulated CPU time (s) 759.74 Current children cumulated vsize (Kb) 21632 [startup+770.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4648 0 0 0 76933 41 0 0 25 0 1 0 1841344534 20484096 4632 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5001 4632 145 145 0 4856 0 [pid=6404] vsize: 20004 Current children cumulated CPU time (s) 769.74 Current children cumulated vsize (Kb) 22128 [startup+780.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4654 0 0 0 77933 41 0 0 25 0 1 0 1841344534 20516864 4638 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5009 4638 145 145 0 4864 0 [pid=6404] vsize: 20036 Current children cumulated CPU time (s) 779.74 Current children cumulated vsize (Kb) 22160 [startup+790.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4657 0 0 0 78933 41 0 0 25 0 1 0 1841344534 20533248 4641 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5013 4641 145 145 0 4868 0 [pid=6404] vsize: 20052 Current children cumulated CPU time (s) 789.74 Current children cumulated vsize (Kb) 22176 [startup+800.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4664 0 0 0 79933 41 0 0 25 0 1 0 1841344534 20566016 4648 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5021 4648 145 145 0 4876 0 [pid=6404] vsize: 20084 Current children cumulated CPU time (s) 799.74 Current children cumulated vsize (Kb) 22208 [startup+810.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4689 0 0 0 80933 41 0 0 25 0 1 0 1841344534 20697088 4673 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5053 4673 145 145 0 4908 0 [pid=6404] vsize: 20212 Current children cumulated CPU time (s) 809.74 Current children cumulated vsize (Kb) 22336 [startup+820.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4706 0 0 0 81933 41 0 0 25 0 1 0 1841344534 20762624 4690 4294967295 134512640 135094434 3221224448 3221223120 134555765 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5069 4690 145 145 0 4924 0 [pid=6404] vsize: 20276 Current children cumulated CPU time (s) 819.74 Current children cumulated vsize (Kb) 22400 [startup+830.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4718 0 0 0 82934 42 0 0 25 0 1 0 1841344534 20828160 4702 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4702 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 829.76 Current children cumulated vsize (Kb) 22464 [startup+840.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4720 0 0 0 83934 42 0 0 25 0 1 0 1841344534 20828160 4704 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4704 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 839.76 Current children cumulated vsize (Kb) 22464 [startup+850.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4721 0 0 0 84934 42 0 0 25 0 1 0 1841344534 20828160 4705 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4705 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 849.76 Current children cumulated vsize (Kb) 22464 [startup+860.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4723 0 0 0 85934 42 0 0 25 0 1 0 1841344534 20828160 4707 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4707 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 859.76 Current children cumulated vsize (Kb) 22464 [startup+870.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4724 0 0 0 86935 42 0 0 25 0 1 0 1841344534 20828160 4708 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4708 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 869.77 Current children cumulated vsize (Kb) 22464 [startup+880.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4724 0 0 0 87935 42 0 0 25 0 1 0 1841344534 20828160 4708 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4708 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 879.77 Current children cumulated vsize (Kb) 22464 [startup+890.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4725 0 0 0 88935 42 0 0 25 0 1 0 1841344534 20828160 4709 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4709 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 889.77 Current children cumulated vsize (Kb) 22464 [startup+900.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4726 0 0 0 89935 42 0 0 25 0 1 0 1841344534 20828160 4710 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5085 4710 145 145 0 4940 0 [pid=6404] vsize: 20340 Current children cumulated CPU time (s) 899.77 Current children cumulated vsize (Kb) 22464 [startup+910.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4758 0 0 0 90935 42 0 0 25 0 1 0 1841344534 20959232 4742 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5117 4742 145 145 0 4972 0 [pid=6404] vsize: 20468 Current children cumulated CPU time (s) 909.77 Current children cumulated vsize (Kb) 22592 [startup+920.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4781 0 0 0 91935 42 0 0 25 0 1 0 1841344534 21045248 4765 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5138 4765 145 145 0 4993 0 [pid=6404] vsize: 20552 Current children cumulated CPU time (s) 919.77 Current children cumulated vsize (Kb) 22676 [startup+930.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 4942 0 0 0 92931 44 0 0 25 0 1 0 1841344534 21729280 4926 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5305 4926 145 145 0 5160 0 [pid=6404] vsize: 21220 Current children cumulated CPU time (s) 929.75 Current children cumulated vsize (Kb) 23344 [startup+940.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5073 0 0 0 93929 45 0 0 25 0 1 0 1841344534 22380544 5057 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5464 5057 145 145 0 5319 0 [pid=6404] vsize: 21856 Current children cumulated CPU time (s) 939.74 Current children cumulated vsize (Kb) 23980 [startup+950.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5080 0 0 0 94929 45 0 0 25 0 1 0 1841344534 22413312 5064 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5472 5064 145 145 0 5327 0 [pid=6404] vsize: 21888 Current children cumulated CPU time (s) 949.74 Current children cumulated vsize (Kb) 24012 [startup+960.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5083 0 0 0 95929 45 0 0 25 0 1 0 1841344534 22478848 5067 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5488 5067 145 145 0 5343 0 [pid=6404] vsize: 21952 Current children cumulated CPU time (s) 959.74 Current children cumulated vsize (Kb) 24076 [startup+970.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5083 0 0 0 96930 45 0 0 25 0 1 0 1841344534 22478848 5067 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5488 5067 145 145 0 5343 0 [pid=6404] vsize: 21952 Current children cumulated CPU time (s) 969.75 Current children cumulated vsize (Kb) 24076 [startup+980.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5089 0 0 0 97930 45 0 0 25 0 1 0 1841344534 22478848 5073 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5488 5073 145 145 0 5343 0 [pid=6404] vsize: 21952 Current children cumulated CPU time (s) 979.75 Current children cumulated vsize (Kb) 24076 [startup+990.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5241 0 0 0 98928 46 0 0 25 0 1 0 1841344534 23113728 5225 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5643 5225 145 145 0 5498 0 [pid=6404] vsize: 22572 Current children cumulated CPU time (s) 989.74 Current children cumulated vsize (Kb) 24696 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5484 0 0 0 99924 48 0 0 25 0 1 0 1841344534 24109056 5468 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5886 5468 145 145 0 5741 0 [pid=6404] vsize: 23544 Current children cumulated CPU time (s) 999.72 Current children cumulated vsize (Kb) 25668 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 100923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223104 134558174 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0 [pid=6404] vsize: 23748 Current children cumulated CPU time (s) 1009.71 Current children cumulated vsize (Kb) 25872 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 101923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0 [pid=6404] vsize: 23748 Current children cumulated CPU time (s) 1019.71 Current children cumulated vsize (Kb) 25872 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5535 0 0 0 102923 48 0 0 25 0 1 0 1841344534 24317952 5519 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5937 5519 145 145 0 5792 0 [pid=6404] vsize: 23748 Current children cumulated CPU time (s) 1029.71 Current children cumulated vsize (Kb) 25872 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5536 0 0 0 103923 48 0 0 25 0 1 0 1841344534 24317952 5520 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5937 5520 145 145 0 5792 0 [pid=6404] vsize: 23748 Current children cumulated CPU time (s) 1039.71 Current children cumulated vsize (Kb) 25872 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5577 0 0 0 104924 48 0 0 25 0 1 0 1841344534 24514560 5561 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 5985 5561 145 145 0 5840 0 [pid=6404] vsize: 23940 Current children cumulated CPU time (s) 1049.72 Current children cumulated vsize (Kb) 26064 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5725 0 0 0 105921 49 0 0 25 0 1 0 1841344534 25116672 5709 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6132 5709 145 145 0 5987 0 [pid=6404] vsize: 24528 Current children cumulated CPU time (s) 1059.7 Current children cumulated vsize (Kb) 26652 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5943 0 0 0 106918 51 0 0 25 0 1 0 1841344534 26038272 5927 4294967295 134512640 135094434 3221224448 3221223040 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6357 5927 145 145 0 6212 0 [pid=6404] vsize: 25428 Current children cumulated CPU time (s) 1069.69 Current children cumulated vsize (Kb) 27552 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5951 0 0 0 107918 51 0 0 25 0 1 0 1841344534 26071040 5935 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6365 5935 145 145 0 6220 0 [pid=6404] vsize: 25460 Current children cumulated CPU time (s) 1079.69 Current children cumulated vsize (Kb) 27584 [startup+1090.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5951 0 0 0 108918 51 0 0 25 0 1 0 1841344534 26071040 5935 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6365 5935 145 145 0 6220 0 [pid=6404] vsize: 25460 Current children cumulated CPU time (s) 1089.69 Current children cumulated vsize (Kb) 27584 [startup+1100.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5956 0 0 0 109918 51 0 0 25 0 1 0 1841344534 26103808 5940 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6373 5940 145 145 0 6228 0 [pid=6404] vsize: 25492 Current children cumulated CPU time (s) 1099.69 Current children cumulated vsize (Kb) 27616 [startup+1110.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5956 0 0 0 110919 51 0 0 25 0 1 0 1841344534 26103808 5940 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6373 5940 145 145 0 6228 0 [pid=6404] vsize: 25492 Current children cumulated CPU time (s) 1109.7 Current children cumulated vsize (Kb) 27616 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5963 0 0 0 111919 51 0 0 25 0 1 0 1841344534 26136576 5947 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6381 5947 145 145 0 6236 0 [pid=6404] vsize: 25524 Current children cumulated CPU time (s) 1119.7 Current children cumulated vsize (Kb) 27648 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 112919 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0 [pid=6404] vsize: 25588 Current children cumulated CPU time (s) 1129.7 Current children cumulated vsize (Kb) 27712 [startup+1140.11 s] Raw data (loadavg): 1.07 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 113919 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0 [pid=6404] vsize: 25588 Current children cumulated CPU time (s) 1139.7 Current children cumulated vsize (Kb) 27712 [startup+1150.11 s] Raw data (loadavg): 1.06 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5977 0 0 0 114920 51 0 0 25 0 1 0 1841344534 26202112 5961 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6397 5961 145 145 0 6252 0 [pid=6404] vsize: 25588 Current children cumulated CPU time (s) 1149.71 Current children cumulated vsize (Kb) 27712 [startup+1160.11 s] Raw data (loadavg): 1.05 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5978 0 0 0 115920 51 0 0 25 0 1 0 1841344534 26202112 5962 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6397 5962 145 145 0 6252 0 [pid=6404] vsize: 25588 Current children cumulated CPU time (s) 1159.71 Current children cumulated vsize (Kb) 27712 [startup+1170.11 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 5989 0 0 0 116920 51 0 0 25 0 1 0 1841344534 26267648 5973 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6413 5973 145 145 0 6268 0 [pid=6404] vsize: 25652 Current children cumulated CPU time (s) 1169.71 Current children cumulated vsize (Kb) 27776 [startup+1180.11 s] Raw data (loadavg): 1.04 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6000 0 0 0 117920 51 0 0 25 0 1 0 1841344534 26333184 5984 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6429 5984 145 145 0 6284 0 [pid=6404] vsize: 25716 Current children cumulated CPU time (s) 1179.71 Current children cumulated vsize (Kb) 27840 [startup+1190.11 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6001 0 0 0 118921 51 0 0 25 0 1 0 1841344534 26333184 5985 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6429 5985 145 145 0 6284 0 [pid=6404] vsize: 25716 Current children cumulated CPU time (s) 1189.72 Current children cumulated vsize (Kb) 27840 [startup+1200.11 s] Raw data (loadavg): 1.03 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 119921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221223104 134558549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0 [pid=6404] vsize: 25716 Current children cumulated CPU time (s) 1199.72 Current children cumulated vsize (Kb) 27840 [startup+1210.11 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 120921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0 [pid=6404] vsize: 25716 Current children cumulated CPU time (s) 1209.72 Current children cumulated vsize (Kb) 27840 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 1.02 0.99 0.91 2/57 6404 Raw data (/proc/6400/stat): 6400 (minisat+_script) S 6399 6400 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1841344529 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/6400/statm): 531 226 485 147 0 384 0 [pid=6400] vsize: 2124 Raw data (/proc/6404/stat): 6404 (minisat+_64-bit) R 6400 6400 2660 0 -1 0 6002 0 0 0 120921 51 0 0 25 0 1 0 1841344534 26333184 5986 4294967295 134512640 135094434 3221224448 3221222912 134781560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6404/statm): 6429 5986 145 145 0 6284 0 [pid=6404] vsize: 25716 Current children cumulated CPU time (s) 1209.72 Current children cumulated vsize (Kb) 27840 Sending SIGTERM to -6400 Sleeping 2 seconds One traced child (pid=6400) ended because it received signal 15 (SIGTERM) One traced child (pid=6404) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.13 CPU time (s): 1209.75 CPU user time (s): 1209.22 CPU system time (s): 0.529919 CPU usage (%): 99.9683 Max. virtual memory (cumulated for all children) (Kb): 27840
ERROR: no interpretation found !