Name | submitted/manquinho/primes-dimacs-cnf/normalized-par32-1-c.opb |
MD5SUM | 8c1b8634a2f99e9f8e579ef031d10353 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 2630 |
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 | 2630 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2630 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 2630 |
Total number of constraints | 6569 |
Number of constraints which are clauses | 6569 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 3 |
LAUNCH ON wulflinc30 THE 2005-09-18 15:30:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2534 boxname=wulflinc30 idbench=190 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c1b8634a2f99e9f8e579ef031d10353 /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb IDLAUNCH: 2534 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 909812 kB Buffers: 37220 kB Cached: 57464 kB SwapCached: 788 kB Active: 62584 kB Inactive: 34808 kB HighTotal: 131008 kB HighFree: 72744 kB LowTotal: 903652 kB LowFree: 837068 kB SwapTotal: 2097892 kB SwapFree: 2096636 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 21932 kB Committed_AS: 64136 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:50:13 (client local time) WITH STATUS 0 IN 1200.14 SECONDS stats: 2534 7 1200.14 0
c Parsing PB file... c Converting 6569 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 | 6569 18020 | 2189 0 0 nan | 0.000 % | c | 100 | 6569 18020 | 2407 100 3667 36.7 | 0.004 % | c | 251 | 6569 18020 | 2648 251 9998 39.8 | 0.000 % | c | 477 | 6569 18020 | 2913 477 19389 40.6 | 0.000 % | c | 814 | 6569 18020 | 3204 814 28997 35.6 | 0.000 % | c | 1320 | 6569 18020 | 3525 1320 43427 32.9 | 0.000 % | c | 2079 | 6562 18004 | 3877 2077 64872 31.2 | 0.076 % | c | 3218 | 6562 18004 | 4265 3216 92939 28.9 | 0.076 % | c | 4927 | 6562 18004 | 4692 2772 64097 23.1 | 0.076 % | c | 7489 | 6562 18004 | 5161 2951 64576 21.9 | 0.076 % | c | 11333 | 6562 18004 | 5677 4187 97402 23.3 | 0.076 % | c | 17099 | 6562 18004 | 6245 4190 93186 22.2 | 0.076 % | c | 25748 | 6562 18004 | 6870 3311 68434 20.7 | 0.076 % | c | 38722 | 6562 18004 | 7557 5903 133047 22.5 | 0.076 % | c | 58183 | 6562 18004 | 8312 6287 144714 23.0 | 0.076 % | c | 87376 | 6562 18004 | 9143 6021 133526 22.2 | 0.076 % | c | 131166 | 6562 18004 | 10058 8376 183814 21.9 | 0.076 % | c | 196850 | 6562 18004 | 11064 8127 172744 21.3 | 0.076 % | c | 295376 | 6562 18004 | 12170 6300 144154 22.9 | 0.076 % | c | 443166 | 6562 18004 | 13387 6996 179583 25.7 | 0.076 % | c | 664849 | 6562 18004 | 14726 13043 279106 21.4 | 0.076 % |
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/12262/stat): 12262 (minisat+_script) R 12261 12262 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842334374 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/12262/statm): 174 3 169 147 0 27 0 [pid=12262] 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=12263 New process pid=12264 New process pid=12265 One traced child (pid=12264) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=12265) exited with status: 0 One traced child (pid=12263) exited with status: 0 New process pid=12266 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-par32-1-c.opb [startup+10.0038 s] Raw data (loadavg): 0.70 0.87 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 989 3 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 9.92 Current children cumulated vsize (Kb) 5352 [startup+20.0046 s] Raw data (loadavg): 0.75 0.88 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 1989 4 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 5352 [startup+30.0064 s] Raw data (loadavg): 0.79 0.88 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 2988 4 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223040 134551925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 29.92 Current children cumulated vsize (Kb) 5352 [startup+40.0072 s] Raw data (loadavg): 0.82 0.88 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 3988 5 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 39.93 Current children cumulated vsize (Kb) 5352 [startup+50.009 s] Raw data (loadavg): 0.85 0.89 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 4988 5 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 49.93 Current children cumulated vsize (Kb) 5352 [startup+60.0098 s] Raw data (loadavg): 0.87 0.89 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 733 0 0 0 5988 5 0 0 25 0 1 0 1842334378 3305472 720 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 807 720 145 145 0 662 0 [pid=12266] vsize: 3228 Current children cumulated CPU time (s) 59.93 Current children cumulated vsize (Kb) 5352 [startup+70.0106 s] Raw data (loadavg): 0.89 0.89 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 756 0 0 0 6987 6 0 0 25 0 1 0 1842334378 3432448 743 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 838 743 145 145 0 693 0 [pid=12266] vsize: 3352 Current children cumulated CPU time (s) 69.93 Current children cumulated vsize (Kb) 5476 [startup+80.0124 s] Raw data (loadavg): 0.91 0.90 0.88 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 758 0 0 0 7987 6 0 0 25 0 1 0 1842334378 3465216 745 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 846 745 145 145 0 701 0 [pid=12266] vsize: 3384 Current children cumulated CPU time (s) 79.93 Current children cumulated vsize (Kb) 5508 [startup+90.0132 s] Raw data (loadavg): 0.92 0.90 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 758 0 0 0 8987 6 0 0 25 0 1 0 1842334378 3465216 745 4294967295 134512640 135094434 3221224448 3221223120 134555337 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 846 745 145 145 0 701 0 [pid=12266] vsize: 3384 Current children cumulated CPU time (s) 89.93 Current children cumulated vsize (Kb) 5508 [startup+100.015 s] Raw data (loadavg): 0.93 0.90 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 761 0 0 0 9986 7 0 0 25 0 1 0 1842334378 3465216 748 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 846 748 145 145 0 701 0 [pid=12266] vsize: 3384 Current children cumulated CPU time (s) 99.93 Current children cumulated vsize (Kb) 5508 [startup+110.017 s] Raw data (loadavg): 0.94 0.90 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 788 0 0 0 10985 8 0 0 25 0 1 0 1842334378 3575808 775 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 873 775 145 145 0 728 0 [pid=12266] vsize: 3492 Current children cumulated CPU time (s) 109.93 Current children cumulated vsize (Kb) 5616 [startup+120.018 s] Raw data (loadavg): 0.95 0.91 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 788 0 0 0 11985 9 0 0 25 0 1 0 1842334378 3575808 775 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 873 775 145 145 0 728 0 [pid=12266] vsize: 3492 Current children cumulated CPU time (s) 119.94 Current children cumulated vsize (Kb) 5616 [startup+130.018 s] Raw data (loadavg): 0.96 0.91 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 790 0 0 0 12985 9 0 0 25 0 1 0 1842334378 3584000 777 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 875 777 145 145 0 730 0 [pid=12266] vsize: 3500 Current children cumulated CPU time (s) 129.94 Current children cumulated vsize (Kb) 5624 [startup+140.019 s] Raw data (loadavg): 0.96 0.91 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 798 0 0 0 13984 10 0 0 25 0 1 0 1842334378 3620864 785 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 884 785 145 145 0 739 0 [pid=12266] vsize: 3536 Current children cumulated CPU time (s) 139.94 Current children cumulated vsize (Kb) 5660 [startup+150.021 s] Raw data (loadavg): 0.97 0.91 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 799 0 0 0 14984 10 0 0 25 0 1 0 1842334378 3620864 786 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 884 786 145 145 0 739 0 [pid=12266] vsize: 3536 Current children cumulated CPU time (s) 149.94 Current children cumulated vsize (Kb) 5660 [startup+160.022 s] Raw data (loadavg): 0.97 0.92 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 828 0 0 0 15983 10 0 0 25 0 1 0 1842334378 3739648 815 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 913 815 145 145 0 768 0 [pid=12266] vsize: 3652 Current children cumulated CPU time (s) 159.93 Current children cumulated vsize (Kb) 5776 [startup+170.023 s] Raw data (loadavg): 0.98 0.92 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 844 0 0 0 16982 11 0 0 25 0 1 0 1842334378 3805184 831 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 929 831 145 145 0 784 0 [pid=12266] vsize: 3716 Current children cumulated CPU time (s) 169.93 Current children cumulated vsize (Kb) 5840 [startup+180.024 s] Raw data (loadavg): 0.98 0.92 0.89 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 848 0 0 0 17982 12 0 0 25 0 1 0 1842334378 3821568 835 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 933 835 145 145 0 788 0 [pid=12266] vsize: 3732 Current children cumulated CPU time (s) 179.94 Current children cumulated vsize (Kb) 5856 [startup+190.025 s] Raw data (loadavg): 0.98 0.92 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 855 0 0 0 18981 12 0 0 25 0 1 0 1842334378 3854336 842 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 941 842 145 145 0 796 0 [pid=12266] vsize: 3764 Current children cumulated CPU time (s) 189.93 Current children cumulated vsize (Kb) 5888 [startup+200.027 s] Raw data (loadavg): 0.98 0.92 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 855 0 0 0 19981 13 0 0 25 0 1 0 1842334378 3854336 842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 941 842 145 145 0 796 0 [pid=12266] vsize: 3764 Current children cumulated CPU time (s) 199.94 Current children cumulated vsize (Kb) 5888 [startup+210.028 s] Raw data (loadavg): 0.99 0.93 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 855 0 0 0 20980 14 0 0 25 0 1 0 1842334378 3854336 842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 941 842 145 145 0 796 0 [pid=12266] vsize: 3764 Current children cumulated CPU time (s) 209.94 Current children cumulated vsize (Kb) 5888 [startup+220.028 s] Raw data (loadavg): 0.99 0.93 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 855 0 0 0 21980 14 0 0 25 0 1 0 1842334378 3854336 842 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 941 842 145 145 0 796 0 [pid=12266] vsize: 3764 Current children cumulated CPU time (s) 219.94 Current children cumulated vsize (Kb) 5888 [startup+230.03 s] Raw data (loadavg): 0.99 0.93 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 855 0 0 0 22980 14 0 0 25 0 1 0 1842334378 3854336 842 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 941 842 145 145 0 796 0 [pid=12266] vsize: 3764 Current children cumulated CPU time (s) 229.94 Current children cumulated vsize (Kb) 5888 [startup+240.031 s] Raw data (loadavg): 0.99 0.93 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 881 0 0 0 23979 15 0 0 25 0 1 0 1842334378 3960832 868 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 967 868 145 145 0 822 0 [pid=12266] vsize: 3868 Current children cumulated CPU time (s) 239.94 Current children cumulated vsize (Kb) 5992 [startup+250.033 s] Raw data (loadavg): 0.99 0.93 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 898 0 0 0 24978 16 0 0 25 0 1 0 1842334378 4026368 885 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 983 885 145 145 0 838 0 [pid=12266] vsize: 3932 Current children cumulated CPU time (s) 249.94 Current children cumulated vsize (Kb) 6056 [startup+260.035 s] Raw data (loadavg): 0.99 0.94 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 898 0 0 0 25978 16 0 0 25 0 1 0 1842334378 4026368 885 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 983 885 145 145 0 838 0 [pid=12266] vsize: 3932 Current children cumulated CPU time (s) 259.94 Current children cumulated vsize (Kb) 6056 [startup+270.035 s] Raw data (loadavg): 0.99 0.94 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 909 0 0 0 26977 17 0 0 25 0 1 0 1842334378 4091904 896 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 999 896 145 145 0 854 0 [pid=12266] vsize: 3996 Current children cumulated CPU time (s) 269.94 Current children cumulated vsize (Kb) 6120 [startup+280.037 s] Raw data (loadavg): 0.99 0.94 0.90 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 914 0 0 0 27977 17 0 0 25 0 1 0 1842334378 4112384 901 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1004 901 145 145 0 859 0 [pid=12266] vsize: 4016 Current children cumulated CPU time (s) 279.94 Current children cumulated vsize (Kb) 6140 [startup+290.039 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 932 0 0 0 28976 18 0 0 25 0 1 0 1842334378 4194304 919 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1024 919 145 145 0 879 0 [pid=12266] vsize: 4096 Current children cumulated CPU time (s) 289.94 Current children cumulated vsize (Kb) 6220 [startup+300.041 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 932 0 0 0 29976 19 0 0 25 0 1 0 1842334378 4194304 919 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1024 919 145 145 0 879 0 [pid=12266] vsize: 4096 Current children cumulated CPU time (s) 299.95 Current children cumulated vsize (Kb) 6220 [startup+310.042 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 938 0 0 0 30975 19 0 0 25 0 1 0 1842334378 4227072 925 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1032 925 145 145 0 887 0 [pid=12266] vsize: 4128 Current children cumulated CPU time (s) 309.94 Current children cumulated vsize (Kb) 6252 [startup+320.042 s] Raw data (loadavg): 0.99 0.94 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 944 0 0 0 31975 20 0 0 25 0 1 0 1842334378 4259840 931 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1040 931 145 145 0 895 0 [pid=12266] vsize: 4160 Current children cumulated CPU time (s) 319.95 Current children cumulated vsize (Kb) 6284 [startup+330.044 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 949 0 0 0 32974 20 0 0 25 0 1 0 1842334378 4292608 936 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1048 936 145 145 0 903 0 [pid=12266] vsize: 4192 Current children cumulated CPU time (s) 329.94 Current children cumulated vsize (Kb) 6316 [startup+340.045 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 949 0 0 0 33974 21 0 0 25 0 1 0 1842334378 4292608 936 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1048 936 145 145 0 903 0 [pid=12266] vsize: 4192 Current children cumulated CPU time (s) 339.95 Current children cumulated vsize (Kb) 6316 [startup+350.047 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 949 0 0 0 34974 21 0 0 25 0 1 0 1842334378 4292608 936 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1048 936 145 145 0 903 0 [pid=12266] vsize: 4192 Current children cumulated CPU time (s) 349.95 Current children cumulated vsize (Kb) 6316 [startup+360.049 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 953 0 0 0 35973 22 0 0 25 0 1 0 1842334378 4308992 940 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1052 940 145 145 0 907 0 [pid=12266] vsize: 4208 Current children cumulated CPU time (s) 359.95 Current children cumulated vsize (Kb) 6332 [startup+370.049 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 959 0 0 0 36973 22 0 0 25 0 1 0 1842334378 4341760 946 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1060 946 145 145 0 915 0 [pid=12266] vsize: 4240 Current children cumulated CPU time (s) 369.95 Current children cumulated vsize (Kb) 6364 [startup+380.051 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 996 0 0 0 37972 23 0 0 25 0 1 0 1842334378 4493312 983 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1097 983 145 145 0 952 0 [pid=12266] vsize: 4388 Current children cumulated CPU time (s) 379.95 Current children cumulated vsize (Kb) 6512 [startup+390.052 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1008 0 0 0 38971 24 0 0 25 0 1 0 1842334378 4542464 995 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1109 995 145 145 0 964 0 [pid=12266] vsize: 4436 Current children cumulated CPU time (s) 389.95 Current children cumulated vsize (Kb) 6560 [startup+400.054 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1008 0 0 0 39971 24 0 0 25 0 1 0 1842334378 4542464 995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1109 995 145 145 0 964 0 [pid=12266] vsize: 4436 Current children cumulated CPU time (s) 399.95 Current children cumulated vsize (Kb) 6560 [startup+410.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1008 0 0 0 40971 24 0 0 25 0 1 0 1842334378 4542464 995 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1109 995 145 145 0 964 0 [pid=12266] vsize: 4436 Current children cumulated CPU time (s) 409.95 Current children cumulated vsize (Kb) 6560 [startup+420.055 s] Raw data (loadavg): 0.99 0.95 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1010 0 0 0 41972 24 0 0 25 0 1 0 1842334378 4558848 997 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1113 997 145 145 0 968 0 [pid=12266] vsize: 4452 Current children cumulated CPU time (s) 419.96 Current children cumulated vsize (Kb) 6576 [startup+430.056 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1012 0 0 0 42971 25 0 0 25 0 1 0 1842334378 4567040 999 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1115 999 145 145 0 970 0 [pid=12266] vsize: 4460 Current children cumulated CPU time (s) 429.96 Current children cumulated vsize (Kb) 6584 [startup+440.057 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1014 0 0 0 43972 25 0 0 25 0 1 0 1842334378 4575232 1001 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1117 1001 145 145 0 972 0 [pid=12266] vsize: 4468 Current children cumulated CPU time (s) 439.97 Current children cumulated vsize (Kb) 6592 [startup+450.058 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1018 0 0 0 44972 25 0 0 25 0 1 0 1842334378 4599808 1005 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1123 1005 145 145 0 978 0 [pid=12266] vsize: 4492 Current children cumulated CPU time (s) 449.97 Current children cumulated vsize (Kb) 6616 [startup+460.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1018 0 0 0 45972 25 0 0 25 0 1 0 1842334378 4599808 1005 4294967295 134512640 135094434 3221224448 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1123 1005 145 145 0 978 0 [pid=12266] vsize: 4492 Current children cumulated CPU time (s) 459.97 Current children cumulated vsize (Kb) 6616 [startup+470.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1030 0 0 0 46972 25 0 0 25 0 1 0 1842334378 4644864 1017 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1134 1017 145 145 0 989 0 [pid=12266] vsize: 4536 Current children cumulated CPU time (s) 469.97 Current children cumulated vsize (Kb) 6660 [startup+480.06 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1038 0 0 0 47972 25 0 0 25 0 1 0 1842334378 4685824 1025 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1144 1025 145 145 0 999 0 [pid=12266] vsize: 4576 Current children cumulated CPU time (s) 479.97 Current children cumulated vsize (Kb) 6700 [startup+490.061 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 48972 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 489.97 Current children cumulated vsize (Kb) 6732 [startup+500.063 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 49972 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 499.97 Current children cumulated vsize (Kb) 6732 [startup+510.063 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 50973 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 509.98 Current children cumulated vsize (Kb) 6732 [startup+520.064 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 51973 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 519.98 Current children cumulated vsize (Kb) 6732 [startup+530.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 52973 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223104 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 529.98 Current children cumulated vsize (Kb) 6732 [startup+540.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1044 0 0 0 53973 25 0 0 25 0 1 0 1842334378 4718592 1031 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1031 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 539.98 Current children cumulated vsize (Kb) 6732 [startup+550.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1045 0 0 0 54974 25 0 0 25 0 1 0 1842334378 4718592 1032 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1152 1032 145 145 0 1007 0 [pid=12266] vsize: 4608 Current children cumulated CPU time (s) 549.99 Current children cumulated vsize (Kb) 6732 [startup+560.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1062 0 0 0 55973 26 0 0 25 0 1 0 1842334378 4792320 1049 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12266/statm): 1170 1049 145 145 0 1025 0 [pid=12266] vsize: 4680 Current children cumulated CPU time (s) 559.99 Current children cumulated vsize (Kb) 6804 [startup+570.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1067 0 0 0 56972 26 0 0 25 0 1 0 1842334378 4804608 1054 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1173 1054 145 145 0 1028 0 [pid=12266] vsize: 4692 Current children cumulated CPU time (s) 569.98 Current children cumulated vsize (Kb) 6816 [startup+580.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1073 0 0 0 57972 26 0 0 25 0 1 0 1842334378 4829184 1060 4294967295 134512640 135094434 3221224448 3221223072 134562095 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1179 1060 145 145 0 1034 0 [pid=12266] vsize: 4716 Current children cumulated CPU time (s) 579.98 Current children cumulated vsize (Kb) 6840 [startup+590.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1080 0 0 0 58972 26 0 0 25 0 1 0 1842334378 4861952 1067 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1187 1067 145 145 0 1042 0 [pid=12266] vsize: 4748 Current children cumulated CPU time (s) 589.98 Current children cumulated vsize (Kb) 6872 [startup+600.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1086 0 0 0 59973 26 0 0 25 0 1 0 1842334378 4894720 1073 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1195 1073 145 145 0 1050 0 [pid=12266] vsize: 4780 Current children cumulated CPU time (s) 599.99 Current children cumulated vsize (Kb) 6904 [startup+610.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1092 0 0 0 60973 26 0 0 25 0 1 0 1842334378 4927488 1079 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1203 1079 145 145 0 1058 0 [pid=12266] vsize: 4812 Current children cumulated CPU time (s) 609.99 Current children cumulated vsize (Kb) 6936 [startup+620.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1093 0 0 0 61973 26 0 0 25 0 1 0 1842334378 4927488 1080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1203 1080 145 145 0 1058 0 [pid=12266] vsize: 4812 Current children cumulated CPU time (s) 619.99 Current children cumulated vsize (Kb) 6936 [startup+630.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1094 0 0 0 62973 26 0 0 25 0 1 0 1842334378 4927488 1081 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1203 1081 145 145 0 1058 0 [pid=12266] vsize: 4812 Current children cumulated CPU time (s) 629.99 Current children cumulated vsize (Kb) 6936 [startup+640.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1094 0 0 0 63973 26 0 0 25 0 1 0 1842334378 4927488 1081 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1203 1081 145 145 0 1058 0 [pid=12266] vsize: 4812 Current children cumulated CPU time (s) 639.99 Current children cumulated vsize (Kb) 6936 [startup+650.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1100 0 0 0 64974 26 0 0 25 0 1 0 1842334378 4960256 1087 4294967295 134512640 135094434 3221224448 3221223104 134557820 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1211 1087 145 145 0 1066 0 [pid=12266] vsize: 4844 Current children cumulated CPU time (s) 650 Current children cumulated vsize (Kb) 6968 [startup+660.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1100 0 0 0 65974 26 0 0 25 0 1 0 1842334378 4960256 1087 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1211 1087 145 145 0 1066 0 [pid=12266] vsize: 4844 Current children cumulated CPU time (s) 660 Current children cumulated vsize (Kb) 6968 [startup+670.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1106 0 0 0 66974 26 0 0 25 0 1 0 1842334378 4993024 1093 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1219 1093 145 145 0 1074 0 [pid=12266] vsize: 4876 Current children cumulated CPU time (s) 670 Current children cumulated vsize (Kb) 7000 [startup+680.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1106 0 0 0 67974 26 0 0 25 0 1 0 1842334378 4993024 1093 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1219 1093 145 145 0 1074 0 [pid=12266] vsize: 4876 Current children cumulated CPU time (s) 680 Current children cumulated vsize (Kb) 7000 [startup+690.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1112 0 0 0 68974 26 0 0 25 0 1 0 1842334378 5025792 1099 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1227 1099 145 145 0 1082 0 [pid=12266] vsize: 4908 Current children cumulated CPU time (s) 690 Current children cumulated vsize (Kb) 7032 [startup+700.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1112 0 0 0 69975 26 0 0 25 0 1 0 1842334378 5025792 1099 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1227 1099 145 145 0 1082 0 [pid=12266] vsize: 4908 Current children cumulated CPU time (s) 700.01 Current children cumulated vsize (Kb) 7032 [startup+710.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1114 0 0 0 70975 26 0 0 25 0 1 0 1842334378 5025792 1101 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1227 1101 145 145 0 1082 0 [pid=12266] vsize: 4908 Current children cumulated CPU time (s) 710.01 Current children cumulated vsize (Kb) 7032 [startup+720.084 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1124 0 0 0 71975 27 0 0 25 0 1 0 1842334378 5074944 1111 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1239 1111 145 145 0 1094 0 [pid=12266] vsize: 4956 Current children cumulated CPU time (s) 720.02 Current children cumulated vsize (Kb) 7080 [startup+730.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1126 0 0 0 72975 27 0 0 25 0 1 0 1842334378 5074944 1113 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1239 1113 145 145 0 1094 0 [pid=12266] vsize: 4956 Current children cumulated CPU time (s) 730.02 Current children cumulated vsize (Kb) 7080 [startup+740.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1132 0 0 0 73975 27 0 0 25 0 1 0 1842334378 5107712 1119 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1247 1119 145 145 0 1102 0 [pid=12266] vsize: 4988 Current children cumulated CPU time (s) 740.02 Current children cumulated vsize (Kb) 7112 [startup+750.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 74974 28 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 750.02 Current children cumulated vsize (Kb) 7144 [startup+760.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 75974 28 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 760.02 Current children cumulated vsize (Kb) 7144 [startup+770.087 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 76974 29 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 770.03 Current children cumulated vsize (Kb) 7144 [startup+780.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 77974 29 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 780.03 Current children cumulated vsize (Kb) 7144 [startup+790.089 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 78974 29 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 790.03 Current children cumulated vsize (Kb) 7144 [startup+800.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1138 0 0 0 79974 29 0 0 25 0 1 0 1842334378 5140480 1125 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1255 1125 145 145 0 1110 0 [pid=12266] vsize: 5020 Current children cumulated CPU time (s) 800.03 Current children cumulated vsize (Kb) 7144 [startup+810.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1158 0 0 0 80973 30 0 0 25 0 1 0 1842334378 5214208 1145 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1273 1145 145 145 0 1128 0 [pid=12266] vsize: 5092 Current children cumulated CPU time (s) 810.03 Current children cumulated vsize (Kb) 7216 [startup+820.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1180 0 0 0 81973 30 0 0 25 0 1 0 1842334378 5312512 1167 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1297 1167 145 145 0 1152 0 [pid=12266] vsize: 5188 Current children cumulated CPU time (s) 820.03 Current children cumulated vsize (Kb) 7312 [startup+830.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1190 0 0 0 82973 30 0 0 25 0 1 0 1842334378 5369856 1177 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1311 1177 145 145 0 1166 0 [pid=12266] vsize: 5244 Current children cumulated CPU time (s) 830.03 Current children cumulated vsize (Kb) 7368 [startup+840.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1196 0 0 0 83973 30 0 0 25 0 1 0 1842334378 5402624 1183 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1319 1183 145 145 0 1174 0 [pid=12266] vsize: 5276 Current children cumulated CPU time (s) 840.03 Current children cumulated vsize (Kb) 7400 [startup+850.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1199 0 0 0 84974 30 0 0 25 0 1 0 1842334378 5402624 1186 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1319 1186 145 145 0 1174 0 [pid=12266] vsize: 5276 Current children cumulated CPU time (s) 850.04 Current children cumulated vsize (Kb) 7400 [startup+860.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1204 0 0 0 85974 31 0 0 25 0 1 0 1842334378 5419008 1191 4294967295 134512640 135094434 3221224448 3221223072 134557574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1323 1191 145 145 0 1178 0 [pid=12266] vsize: 5292 Current children cumulated CPU time (s) 860.05 Current children cumulated vsize (Kb) 7416 [startup+870.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1220 0 0 0 86974 31 0 0 25 0 1 0 1842334378 5496832 1207 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1342 1207 145 145 0 1197 0 [pid=12266] vsize: 5368 Current children cumulated CPU time (s) 870.05 Current children cumulated vsize (Kb) 7492 [startup+880.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1222 0 0 0 87974 31 0 0 25 0 1 0 1842334378 5496832 1209 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1342 1209 145 145 0 1197 0 [pid=12266] vsize: 5368 Current children cumulated CPU time (s) 880.05 Current children cumulated vsize (Kb) 7492 [startup+890.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1222 0 0 0 88974 31 0 0 25 0 1 0 1842334378 5496832 1209 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1342 1209 145 145 0 1197 0 [pid=12266] vsize: 5368 Current children cumulated CPU time (s) 890.05 Current children cumulated vsize (Kb) 7492 [startup+900.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1227 0 0 0 89974 31 0 0 25 0 1 0 1842334378 5529600 1214 4294967295 134512640 135094434 3221224448 3221222976 134783007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1350 1214 145 145 0 1205 0 [pid=12266] vsize: 5400 Current children cumulated CPU time (s) 900.05 Current children cumulated vsize (Kb) 7524 [startup+910.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1228 0 0 0 90974 31 0 0 25 0 1 0 1842334378 5529600 1215 4294967295 134512640 135094434 3221224448 3221223072 134557734 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1350 1215 145 145 0 1205 0 [pid=12266] vsize: 5400 Current children cumulated CPU time (s) 910.05 Current children cumulated vsize (Kb) 7524 [startup+920.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1228 0 0 0 91975 31 0 0 25 0 1 0 1842334378 5529600 1215 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1350 1215 145 145 0 1205 0 [pid=12266] vsize: 5400 Current children cumulated CPU time (s) 920.06 Current children cumulated vsize (Kb) 7524 [startup+930.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1246 0 0 0 92974 31 0 0 25 0 1 0 1842334378 5603328 1233 4294967295 134512640 135094434 3221224448 3221223120 134555544 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1368 1233 145 145 0 1223 0 [pid=12266] vsize: 5472 Current children cumulated CPU time (s) 930.05 Current children cumulated vsize (Kb) 7596 [startup+940.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1261 0 0 0 93975 31 0 0 25 0 1 0 1842334378 5664768 1248 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1383 1248 145 145 0 1238 0 [pid=12266] vsize: 5532 Current children cumulated CPU time (s) 940.06 Current children cumulated vsize (Kb) 7656 [startup+950.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1266 0 0 0 94975 31 0 0 25 0 1 0 1842334378 5685248 1253 4294967295 134512640 135094434 3221224448 3221223120 134555232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1388 1253 145 145 0 1243 0 [pid=12266] vsize: 5552 Current children cumulated CPU time (s) 950.06 Current children cumulated vsize (Kb) 7676 [startup+960.103 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1266 0 0 0 95975 31 0 0 25 0 1 0 1842334378 5685248 1253 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1388 1253 145 145 0 1243 0 [pid=12266] vsize: 5552 Current children cumulated CPU time (s) 960.06 Current children cumulated vsize (Kb) 7676 [startup+970.104 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1266 0 0 0 96975 31 0 0 25 0 1 0 1842334378 5685248 1253 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1388 1253 145 145 0 1243 0 [pid=12266] vsize: 5552 Current children cumulated CPU time (s) 970.06 Current children cumulated vsize (Kb) 7676 [startup+980.105 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1268 0 0 0 97975 32 0 0 25 0 1 0 1842334378 5693440 1255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1390 1255 145 145 0 1245 0 [pid=12266] vsize: 5560 Current children cumulated CPU time (s) 980.07 Current children cumulated vsize (Kb) 7684 [startup+990.106 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1268 0 0 0 98976 32 0 0 25 0 1 0 1842334378 5693440 1255 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1390 1255 145 145 0 1245 0 [pid=12266] vsize: 5560 Current children cumulated CPU time (s) 990.08 Current children cumulated vsize (Kb) 7684 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1268 0 0 0 99976 32 0 0 25 0 1 0 1842334378 5693440 1255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1390 1255 145 145 0 1245 0 [pid=12266] vsize: 5560 Current children cumulated CPU time (s) 1000.08 Current children cumulated vsize (Kb) 7684 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1268 0 0 0 100976 32 0 0 25 0 1 0 1842334378 5693440 1255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1390 1255 145 145 0 1245 0 [pid=12266] vsize: 5560 Current children cumulated CPU time (s) 1010.08 Current children cumulated vsize (Kb) 7684 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1268 0 0 0 101976 32 0 0 25 0 1 0 1842334378 5693440 1255 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1390 1255 145 145 0 1245 0 [pid=12266] vsize: 5560 Current children cumulated CPU time (s) 1020.08 Current children cumulated vsize (Kb) 7684 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 102976 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1030.08 Current children cumulated vsize (Kb) 7696 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 103976 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1040.08 Current children cumulated vsize (Kb) 7696 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 104977 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1050.09 Current children cumulated vsize (Kb) 7696 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 105977 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1060.09 Current children cumulated vsize (Kb) 7696 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 106977 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1070.09 Current children cumulated vsize (Kb) 7696 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 107977 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1080.09 Current children cumulated vsize (Kb) 7696 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 108977 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1090.09 Current children cumulated vsize (Kb) 7696 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1270 0 0 0 109978 32 0 0 25 0 1 0 1842334378 5705728 1257 4294967295 134512640 135094434 3221224448 3221223120 134555815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1393 1257 145 145 0 1248 0 [pid=12266] vsize: 5572 Current children cumulated CPU time (s) 1100.1 Current children cumulated vsize (Kb) 7696 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 110978 32 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1110.1 Current children cumulated vsize (Kb) 7728 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 111978 32 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1120.1 Current children cumulated vsize (Kb) 7728 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 112978 32 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1130.1 Current children cumulated vsize (Kb) 7728 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 113979 32 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1140.11 Current children cumulated vsize (Kb) 7728 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 114979 32 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1150.11 Current children cumulated vsize (Kb) 7728 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1276 0 0 0 115979 33 0 0 25 0 1 0 1842334378 5738496 1263 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1401 1263 145 145 0 1256 0 [pid=12266] vsize: 5604 Current children cumulated CPU time (s) 1160.12 Current children cumulated vsize (Kb) 7728 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1281 0 0 0 116979 33 0 0 25 0 1 0 1842334378 5771264 1268 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1409 1268 145 145 0 1264 0 [pid=12266] vsize: 5636 Current children cumulated CPU time (s) 1170.12 Current children cumulated vsize (Kb) 7760 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1281 0 0 0 117979 33 0 0 25 0 1 0 1842334378 5771264 1268 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1409 1268 145 145 0 1264 0 [pid=12266] vsize: 5636 Current children cumulated CPU time (s) 1180.12 Current children cumulated vsize (Kb) 7760 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1282 0 0 0 118980 33 0 0 25 0 1 0 1842334378 5771264 1269 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1409 1269 145 145 0 1264 0 [pid=12266] vsize: 5636 Current children cumulated CPU time (s) 1190.13 Current children cumulated vsize (Kb) 7760 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1288 0 0 0 119980 33 0 0 25 0 1 0 1842334378 5804032 1275 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1417 1275 145 145 0 1272 0 [pid=12266] vsize: 5668 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 7792 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 12266 Raw data (/proc/12262/stat): 12262 (minisat+_script) S 12261 12262 5245 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1842334374 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/12262/statm): 531 226 485 147 0 384 0 [pid=12262] vsize: 2124 Raw data (/proc/12266/stat): 12266 (minisat+_64-bit) R 12262 12262 5245 0 -1 0 1288 0 0 0 119980 33 0 0 25 0 1 0 1842334378 5804032 1275 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12266/statm): 1417 1275 145 145 0 1272 0 [pid=12266] vsize: 5668 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 7792 Sending SIGTERM to -12262 Sleeping 2 seconds One traced child (pid=12262) ended because it received signal 15 (SIGTERM) One traced child (pid=12266) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.13 CPU time (s): 1200.14 CPU user time (s): 1199.8 CPU system time (s): 0.333949 CPU usage (%): 100.001 Max. virtual memory (cumulated for all children) (Kb): 7792
ERROR: no interpretation found !