Name | submitted/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb |
MD5SUM | 112c693a7a90a8dc93ad23dc136d9b75 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 22 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.027994 |
Number of variables | 840 |
Total number of constraints | 82 |
Number of constraints which are clauses | 42 |
Number of constraints which are cardinality constraints (but not clauses) | 40 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 21 |
LAUNCH ON wulflinc22 THE 2005-09-18 15:48:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2350 boxname=wulflinc22 idbench=6 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 112c693a7a90a8dc93ad23dc136d9b75 /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_21_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_21_pb.cnf.cr.opb IDLAUNCH: 2350 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 920604 kB Buffers: 33880 kB Cached: 52896 kB SwapCached: 536 kB Active: 62396 kB Inactive: 26940 kB HighTotal: 131008 kB HighFree: 76104 kB LowTotal: 903652 kB LowFree: 844500 kB SwapTotal: 2097892 kB SwapFree: 2096832 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5860 kB Slab: 19048 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 16:08:53 (client local time) WITH STATUS 0 IN 1209.77 SECONDS stats: 2350 7 1209.77 0
c Parsing PB file... c Converting 82 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .......................................... c ---[ 39]---> BDD-cost: 39 c ---[ 38]---> BDD-cost: 39 c ---[ 37]---> BDD-cost: 39 c ---[ 36]---> BDD-cost: 39 c ---[ 35]---> BDD-cost: 39 c ---[ 34]---> BDD-cost: 39 c ---[ 33]---> BDD-cost: 39 c ---[ 32]---> BDD-cost: 39 c ---[ 31]---> BDD-cost: 39 c ---[ 30]---> BDD-cost: 39 c ---[ 29]---> BDD-cost: 39 c ---[ 28]---> BDD-cost: 39 c ---[ 27]---> BDD-cost: 39 c ---[ 26]---> BDD-cost: 39 c ---[ 25]---> BDD-cost: 39 c ---[ 24]---> BDD-cost: 39 c ---[ 23]---> BDD-cost: 39 c ---[ 22]---> BDD-cost: 39 c ---[ 21]---> BDD-cost: 39 c ---[ 20]---> BDD-cost: 39 c ---[ 19]---> BDD-cost: 39 c ---[ 18]---> BDD-cost: 39 c ---[ 17]---> BDD-cost: 39 c ---[ 16]---> BDD-cost: 39 c ---[ 15]---> BDD-cost: 39 c ---[ 14]---> BDD-cost: 39 c ---[ 13]---> BDD-cost: 39 c ---[ 12]---> BDD-cost: 39 c ---[ 11]---> BDD-cost: 39 c ---[ 10]---> BDD-cost: 39 c ---[ 9]---> BDD-cost: 39 c ---[ 8]---> BDD-cost: 39 c ---[ 7]---> BDD-cost: 39 c ---[ 6]---> BDD-cost: 39 c ---[ 5]---> BDD-cost: 39 c ---[ 4]---> BDD-cost: 39 c ---[ 3]---> BDD-cost: 39 c ---[ 2]---> BDD-cost: 39 c ---[ 1]---> BDD-cost: 39 c ---[ 0]---> BDD-cost: 39 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 3882 10840 | 1294 0 0 nan | 0.000 % | c | 105 | 3882 10840 | 1423 105 7385 70.3 | 1.667 % | c | 255 | 3882 10840 | 1565 255 18850 73.9 | 1.667 % | c | 481 | 3882 10840 | 1722 481 40545 84.3 | 1.667 % | c | 818 | 3882 10840 | 1894 818 71265 87.1 | 1.667 % | c | 1330 | 3882 10840 | 2083 1330 131039 98.5 | 1.667 % | c | 2092 | 3882 10840 | 2292 2092 211172 100.9 | 1.667 % | c | 3231 | 3882 10840 | 2521 1659 186225 112.3 | 1.667 % | c | 4942 | 3882 10840 | 2773 3370 365003 108.3 | 1.667 % | c | 7507 | 3882 10840 | 3051 2457 314757 128.1 | 1.667 % | c | 11351 | 3882 10840 | 3356 2383 263788 110.7 | 1.667 % | c | 17118 | 3882 10840 | 3691 3938 513865 130.5 | 1.667 % | c | 25770 | 3882 10840 | 4061 3926 537570 136.9 | 1.667 % | c | 38745 | 3882 10840 | 4467 4621 522096 113.0 | 1.667 % | c | 58208 | 3882 10840 | 4913 3339 584284 175.0 | 1.667 % | c | 87400 | 3882 10840 | 5405 5035 947887 188.3 | 1.667 % | c | 131189 | 3882 10840 | 5945 3280 620922 189.3 | 1.667 % | c | 196874 | 3882 10840 | 6540 5430 876118 161.3 | 1.667 % | c | 295400 | 3882 10840 | 7194 4105 759531 185.0 | 1.667 % | c | 443191 | 3882 10840 | 7913 8832 1414915 160.2 | 1.667 % | c | 664876 | 3882 10840 | 8705 6366 1068393 167.8 | 1.667 % |
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/26654/stat): 26654 (minisat+_script) R 26653 26654 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842458517 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/26654/statm): 174 3 169 147 0 27 0 [pid=26654] 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=26655 New process pid=26656 New process pid=26657 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 One traced child (pid=26656) exited with status: 0 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=26657) exited with status: 0 One traced child (pid=26655) exited with status: 0 New process pid=26658 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-chnl20_21_pb.cnf.cr.opb [startup+10.0046 s] Raw data (loadavg): 0.93 0.95 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1039 0 0 0 984 4 0 0 25 0 1 0 1842458522 4562944 1026 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 1114 1026 145 145 0 969 0 [pid=26658] vsize: 4456 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 6580 [startup+20.0053 s] Raw data (loadavg): 0.94 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1338 0 0 0 1980 6 0 0 25 0 1 0 1842458522 5808128 1325 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 1418 1325 145 145 0 1273 0 [pid=26658] vsize: 5672 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 7796 [startup+30.0071 s] Raw data (loadavg): 0.95 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1375 0 0 0 2979 7 0 0 25 0 1 0 1842458522 5955584 1362 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 1454 1362 145 145 0 1309 0 [pid=26658] vsize: 5816 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 7940 [startup+40.0077 s] Raw data (loadavg): 0.95 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1695 0 0 0 3974 9 0 0 25 0 1 0 1842458522 7274496 1682 4294967295 134512640 135094434 3221224432 3221223056 134557655 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 1776 1682 145 145 0 1631 0 [pid=26658] vsize: 7104 Current children cumulated CPU time (s) 39.84 Current children cumulated vsize (Kb) 9228 [startup+50.0094 s] Raw data (loadavg): 0.96 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1788 0 0 0 4973 9 0 0 25 0 1 0 1842458522 7671808 1775 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 1873 1775 145 145 0 1728 0 [pid=26658] vsize: 7492 Current children cumulated CPU time (s) 49.83 Current children cumulated vsize (Kb) 9616 [startup+60.0102 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1925 0 0 0 5971 10 0 0 25 0 1 0 1842458522 8261632 1912 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2017 1912 145 145 0 1872 0 [pid=26658] vsize: 8068 Current children cumulated CPU time (s) 59.82 Current children cumulated vsize (Kb) 10192 [startup+70.0109 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 1953 0 0 0 6971 10 0 0 25 0 1 0 1842458522 8376320 1940 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2045 1940 145 145 0 1900 0 [pid=26658] vsize: 8180 Current children cumulated CPU time (s) 69.82 Current children cumulated vsize (Kb) 10304 [startup+80.0116 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2246 0 0 0 7965 13 0 0 25 0 1 0 1842458522 9576448 2233 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2338 2233 145 145 0 2193 0 [pid=26658] vsize: 9352 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 11476 [startup+90.0123 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2321 0 0 0 8965 13 0 0 25 0 1 0 1842458522 9887744 2308 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2414 2308 145 145 0 2269 0 [pid=26658] vsize: 9656 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 11780 [startup+100.013 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2322 0 0 0 9964 14 0 0 25 0 1 0 1842458522 9887744 2309 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2414 2309 145 145 0 2269 0 [pid=26658] vsize: 9656 Current children cumulated CPU time (s) 99.79 Current children cumulated vsize (Kb) 11780 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2322 0 0 0 10965 14 0 0 25 0 1 0 1842458522 9887744 2309 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2414 2309 145 145 0 2269 0 [pid=26658] vsize: 9656 Current children cumulated CPU time (s) 109.8 Current children cumulated vsize (Kb) 11780 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2323 0 0 0 11964 14 0 0 25 0 1 0 1842458522 9887744 2310 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2414 2310 145 145 0 2269 0 [pid=26658] vsize: 9656 Current children cumulated CPU time (s) 119.79 Current children cumulated vsize (Kb) 11780 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2492 0 0 0 12961 17 0 0 25 0 1 0 1842458522 10579968 2479 4294967295 134512640 135094434 3221224432 3221223088 134558017 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2583 2479 145 145 0 2438 0 [pid=26658] vsize: 10332 Current children cumulated CPU time (s) 129.79 Current children cumulated vsize (Kb) 12456 [startup+140.016 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 13960 17 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0 [pid=26658] vsize: 10628 Current children cumulated CPU time (s) 139.78 Current children cumulated vsize (Kb) 12752 [startup+150.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 14960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223104 134556502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0 [pid=26658] vsize: 10628 Current children cumulated CPU time (s) 149.79 Current children cumulated vsize (Kb) 12752 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 15960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0 [pid=26658] vsize: 10628 Current children cumulated CPU time (s) 159.79 Current children cumulated vsize (Kb) 12752 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 16960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223104 134556277 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0 [pid=26658] vsize: 10628 Current children cumulated CPU time (s) 169.79 Current children cumulated vsize (Kb) 12752 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2566 0 0 0 17960 18 0 0 25 0 1 0 1842458522 10883072 2553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2657 2553 145 145 0 2512 0 [pid=26658] vsize: 10628 Current children cumulated CPU time (s) 179.79 Current children cumulated vsize (Kb) 12752 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2596 0 0 0 18959 19 0 0 25 0 1 0 1842458522 11001856 2583 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2686 2583 145 145 0 2541 0 [pid=26658] vsize: 10744 Current children cumulated CPU time (s) 189.79 Current children cumulated vsize (Kb) 12868 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2597 0 0 0 19959 19 0 0 25 0 1 0 1842458522 11001856 2584 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 2686 2584 145 145 0 2541 0 [pid=26658] vsize: 10744 Current children cumulated CPU time (s) 199.79 Current children cumulated vsize (Kb) 12868 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 20958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221222912 134781611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0 [pid=26658] vsize: 10744 Current children cumulated CPU time (s) 209.78 Current children cumulated vsize (Kb) 12868 [startup+220.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 21958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0 [pid=26658] vsize: 10744 Current children cumulated CPU time (s) 219.78 Current children cumulated vsize (Kb) 12868 [startup+230.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2599 0 0 0 22958 19 0 0 25 0 1 0 1842458522 11001856 2586 4294967295 134512640 135094434 3221224432 3221223024 134551860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2686 2586 145 145 0 2541 0 [pid=26658] vsize: 10744 Current children cumulated CPU time (s) 229.78 Current children cumulated vsize (Kb) 12868 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2626 0 0 0 23957 20 0 0 25 0 1 0 1842458522 11116544 2613 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2714 2613 145 145 0 2569 0 [pid=26658] vsize: 10856 Current children cumulated CPU time (s) 239.78 Current children cumulated vsize (Kb) 12980 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2701 0 0 0 24957 20 0 0 25 0 1 0 1842458522 11423744 2688 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2789 2688 145 145 0 2644 0 [pid=26658] vsize: 11156 Current children cumulated CPU time (s) 249.78 Current children cumulated vsize (Kb) 13280 [startup+260.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2790 0 0 0 25955 21 0 0 25 0 1 0 1842458522 11788288 2777 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2878 2777 145 145 0 2733 0 [pid=26658] vsize: 11512 Current children cumulated CPU time (s) 259.77 Current children cumulated vsize (Kb) 13636 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2790 0 0 0 26955 21 0 0 25 0 1 0 1842458522 11788288 2777 4294967295 134512640 135094434 3221224432 3221223104 134555748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2878 2777 145 145 0 2733 0 [pid=26658] vsize: 11512 Current children cumulated CPU time (s) 269.77 Current children cumulated vsize (Kb) 13636 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2791 0 0 0 27956 21 0 0 25 0 1 0 1842458522 11788288 2778 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2878 2778 145 145 0 2733 0 [pid=26658] vsize: 11512 Current children cumulated CPU time (s) 279.78 Current children cumulated vsize (Kb) 13636 [startup+290.026 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2889 0 0 0 28954 22 0 0 25 0 1 0 1842458522 12185600 2876 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2975 2876 145 145 0 2830 0 [pid=26658] vsize: 11900 Current children cumulated CPU time (s) 289.77 Current children cumulated vsize (Kb) 14024 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 2889 0 0 0 29954 22 0 0 25 0 1 0 1842458522 12185600 2876 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 2975 2876 145 145 0 2830 0 [pid=26658] vsize: 11900 Current children cumulated CPU time (s) 299.77 Current children cumulated vsize (Kb) 14024 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 30952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0 [pid=26658] vsize: 12428 Current children cumulated CPU time (s) 309.76 Current children cumulated vsize (Kb) 14552 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 31952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0 [pid=26658] vsize: 12428 Current children cumulated CPU time (s) 319.76 Current children cumulated vsize (Kb) 14552 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3021 0 0 0 32952 23 0 0 25 0 1 0 1842458522 12726272 3008 4294967295 134512640 135094434 3221224432 3221223104 134556091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3107 3008 145 145 0 2962 0 [pid=26658] vsize: 12428 Current children cumulated CPU time (s) 329.76 Current children cumulated vsize (Kb) 14552 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3373 0 0 0 33947 25 0 0 25 0 1 0 1842458522 14176256 3360 4294967295 134512640 135094434 3221224432 3221223024 134557163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3461 3360 145 145 0 3316 0 [pid=26658] vsize: 13844 Current children cumulated CPU time (s) 339.73 Current children cumulated vsize (Kb) 15968 [startup+350.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3386 0 0 0 34947 25 0 0 25 0 1 0 1842458522 14229504 3373 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3474 3373 145 145 0 3329 0 [pid=26658] vsize: 13896 Current children cumulated CPU time (s) 349.73 Current children cumulated vsize (Kb) 16020 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 35946 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 359.73 Current children cumulated vsize (Kb) 16220 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 36946 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 369.73 Current children cumulated vsize (Kb) 16220 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 37947 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 379.74 Current children cumulated vsize (Kb) 16220 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3436 0 0 0 38947 26 0 0 25 0 1 0 1842458522 14434304 3423 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3423 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 389.74 Current children cumulated vsize (Kb) 16220 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 39947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 399.74 Current children cumulated vsize (Kb) 16220 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 40947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 409.74 Current children cumulated vsize (Kb) 16220 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 41947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 419.74 Current children cumulated vsize (Kb) 16220 [startup+430.037 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 42947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 429.74 Current children cumulated vsize (Kb) 16220 [startup+440.038 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 43947 26 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 439.74 Current children cumulated vsize (Kb) 16220 [startup+450.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 44948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 449.76 Current children cumulated vsize (Kb) 16220 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 45948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 459.76 Current children cumulated vsize (Kb) 16220 [startup+470.041 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3437 0 0 0 46948 27 0 0 25 0 1 0 1842458522 14434304 3424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3424 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 469.76 Current children cumulated vsize (Kb) 16220 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3438 0 0 0 47948 27 0 0 25 0 1 0 1842458522 14434304 3425 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3425 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 479.76 Current children cumulated vsize (Kb) 16220 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3438 0 0 0 48948 27 0 0 25 0 1 0 1842458522 14434304 3425 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3524 3425 145 145 0 3379 0 [pid=26658] vsize: 14096 Current children cumulated CPU time (s) 489.76 Current children cumulated vsize (Kb) 16220 [startup+500.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3444 0 0 0 49948 27 0 0 25 0 1 0 1842458522 14475264 3431 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3534 3431 145 145 0 3389 0 [pid=26658] vsize: 14136 Current children cumulated CPU time (s) 499.76 Current children cumulated vsize (Kb) 16260 [startup+510.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3474 0 0 0 50948 27 0 0 25 0 1 0 1842458522 14671872 3461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3582 3461 145 145 0 3437 0 [pid=26658] vsize: 14328 Current children cumulated CPU time (s) 509.76 Current children cumulated vsize (Kb) 16452 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3474 0 0 0 51949 27 0 0 25 0 1 0 1842458522 14671872 3461 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3582 3461 145 145 0 3437 0 [pid=26658] vsize: 14328 Current children cumulated CPU time (s) 519.77 Current children cumulated vsize (Kb) 16452 [startup+530.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3475 0 0 0 52948 28 0 0 25 0 1 0 1842458522 14671872 3462 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3582 3462 145 145 0 3437 0 [pid=26658] vsize: 14328 Current children cumulated CPU time (s) 529.77 Current children cumulated vsize (Kb) 16452 [startup+540.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3495 0 0 0 53948 28 0 0 25 0 1 0 1842458522 14802944 3482 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3614 3482 145 145 0 3469 0 [pid=26658] vsize: 14456 Current children cumulated CPU time (s) 539.77 Current children cumulated vsize (Kb) 16580 [startup+550.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3542 0 0 0 54948 28 0 0 25 0 1 0 1842458522 15040512 3529 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3672 3529 145 145 0 3527 0 [pid=26658] vsize: 14688 Current children cumulated CPU time (s) 549.77 Current children cumulated vsize (Kb) 16812 [startup+560.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3553 0 0 0 55948 28 0 0 25 0 1 0 1842458522 15106048 3540 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3688 3540 145 145 0 3543 0 [pid=26658] vsize: 14752 Current children cumulated CPU time (s) 559.77 Current children cumulated vsize (Kb) 16876 [startup+570.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3553 0 0 0 56949 28 0 0 25 0 1 0 1842458522 15106048 3540 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3688 3540 145 145 0 3543 0 [pid=26658] vsize: 14752 Current children cumulated CPU time (s) 569.78 Current children cumulated vsize (Kb) 16876 [startup+580.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3556 0 0 0 57949 28 0 0 25 0 1 0 1842458522 15106048 3543 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3688 3543 145 145 0 3543 0 [pid=26658] vsize: 14752 Current children cumulated CPU time (s) 579.78 Current children cumulated vsize (Kb) 16876 [startup+590.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3563 0 0 0 58949 28 0 0 25 0 1 0 1842458522 15138816 3550 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3696 3550 145 145 0 3551 0 [pid=26658] vsize: 14784 Current children cumulated CPU time (s) 589.78 Current children cumulated vsize (Kb) 16908 [startup+600.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3563 0 0 0 59949 28 0 0 25 0 1 0 1842458522 15138816 3550 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3696 3550 145 145 0 3551 0 [pid=26658] vsize: 14784 Current children cumulated CPU time (s) 599.78 Current children cumulated vsize (Kb) 16908 [startup+610.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3574 0 0 0 60949 29 0 0 25 0 1 0 1842458522 15200256 3561 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 3711 3561 145 145 0 3566 0 [pid=26658] vsize: 14844 Current children cumulated CPU time (s) 609.79 Current children cumulated vsize (Kb) 16968 [startup+620.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 3974 0 0 0 61945 30 0 0 25 0 1 0 1842458522 16842752 3961 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4112 3961 145 145 0 3967 0 [pid=26658] vsize: 16448 Current children cumulated CPU time (s) 619.76 Current children cumulated vsize (Kb) 18572 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4024 0 0 0 62944 31 0 0 25 0 1 0 1842458522 17047552 4011 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4162 4011 145 145 0 4017 0 [pid=26658] vsize: 16648 Current children cumulated CPU time (s) 629.76 Current children cumulated vsize (Kb) 18772 [startup+640.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 63944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0 [pid=26658] vsize: 16648 Current children cumulated CPU time (s) 639.76 Current children cumulated vsize (Kb) 18772 [startup+650.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 64944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0 [pid=26658] vsize: 16648 Current children cumulated CPU time (s) 649.76 Current children cumulated vsize (Kb) 18772 [startup+660.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4025 0 0 0 65944 31 0 0 25 0 1 0 1842458522 17047552 4012 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4162 4012 145 145 0 4017 0 [pid=26658] vsize: 16648 Current children cumulated CPU time (s) 659.76 Current children cumulated vsize (Kb) 18772 [startup+670.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4039 0 0 0 66944 31 0 0 25 0 1 0 1842458522 17104896 4026 4294967295 134512640 135094434 3221224432 3221222840 134782729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4176 4026 145 145 0 4031 0 [pid=26658] vsize: 16704 Current children cumulated CPU time (s) 669.76 Current children cumulated vsize (Kb) 18828 [startup+680.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4039 0 0 0 67944 31 0 0 25 0 1 0 1842458522 17104896 4026 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4176 4026 145 145 0 4031 0 [pid=26658] vsize: 16704 Current children cumulated CPU time (s) 679.76 Current children cumulated vsize (Kb) 18828 [startup+690.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4072 0 0 0 68944 31 0 0 25 0 1 0 1842458522 17256448 4059 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4213 4059 145 145 0 4068 0 [pid=26658] vsize: 16852 Current children cumulated CPU time (s) 689.76 Current children cumulated vsize (Kb) 18976 [startup+700.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4072 0 0 0 69944 32 0 0 25 0 1 0 1842458522 17256448 4059 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4213 4059 145 145 0 4068 0 [pid=26658] vsize: 16852 Current children cumulated CPU time (s) 699.77 Current children cumulated vsize (Kb) 18976 [startup+710.06 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4080 0 0 0 70944 32 0 0 25 0 1 0 1842458522 17289216 4067 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4221 4067 145 145 0 4076 0 [pid=26658] vsize: 16884 Current children cumulated CPU time (s) 709.77 Current children cumulated vsize (Kb) 19008 [startup+720.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4080 0 0 0 71944 33 0 0 25 0 1 0 1842458522 17289216 4067 4294967295 134512640 135094434 3221224432 3221223104 134556515 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4221 4067 145 145 0 4076 0 [pid=26658] vsize: 16884 Current children cumulated CPU time (s) 719.78 Current children cumulated vsize (Kb) 19008 [startup+730.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4101 0 0 0 72943 34 0 0 25 0 1 0 1842458522 17387520 4088 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4245 4088 145 145 0 4100 0 [pid=26658] vsize: 16980 Current children cumulated CPU time (s) 729.78 Current children cumulated vsize (Kb) 19104 [startup+740.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4112 0 0 0 73943 34 0 0 25 0 1 0 1842458522 17453056 4099 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4261 4099 145 145 0 4116 0 [pid=26658] vsize: 17044 Current children cumulated CPU time (s) 739.78 Current children cumulated vsize (Kb) 19168 [startup+750.065 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4119 0 0 0 74943 34 0 0 25 0 1 0 1842458522 17485824 4106 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4269 4106 145 145 0 4124 0 [pid=26658] vsize: 17076 Current children cumulated CPU time (s) 749.78 Current children cumulated vsize (Kb) 19200 [startup+760.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4120 0 0 0 75943 34 0 0 25 0 1 0 1842458522 17485824 4107 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4269 4107 145 145 0 4124 0 [pid=26658] vsize: 17076 Current children cumulated CPU time (s) 759.78 Current children cumulated vsize (Kb) 19200 [startup+770.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 76943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0 [pid=26658] vsize: 17108 Current children cumulated CPU time (s) 769.79 Current children cumulated vsize (Kb) 19232 [startup+780.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 77943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223072 134562165 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0 [pid=26658] vsize: 17108 Current children cumulated CPU time (s) 779.79 Current children cumulated vsize (Kb) 19232 [startup+790.068 s] Raw data (loadavg): 1.07 0.99 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4128 0 0 0 78943 35 0 0 25 0 1 0 1842458522 17518592 4115 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4277 4115 145 145 0 4132 0 [pid=26658] vsize: 17108 Current children cumulated CPU time (s) 789.79 Current children cumulated vsize (Kb) 19232 [startup+800.069 s] Raw data (loadavg): 1.06 0.99 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4139 0 0 0 79942 35 0 0 25 0 1 0 1842458522 17563648 4126 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 4288 4126 145 145 0 4143 0 [pid=26658] vsize: 17152 Current children cumulated CPU time (s) 799.78 Current children cumulated vsize (Kb) 19276 [startup+810.069 s] Raw data (loadavg): 1.05 0.99 0.95 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4169 0 0 0 80941 36 0 0 25 0 1 0 1842458522 17715200 4156 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4325 4156 145 145 0 4180 0 [pid=26658] vsize: 17300 Current children cumulated CPU time (s) 809.78 Current children cumulated vsize (Kb) 19424 [startup+820.07 s] Raw data (loadavg): 1.12 1.00 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4194 0 0 0 81941 36 0 0 25 0 1 0 1842458522 17846272 4181 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4357 4181 145 145 0 4212 0 [pid=26658] vsize: 17428 Current children cumulated CPU time (s) 819.78 Current children cumulated vsize (Kb) 19552 [startup+830.071 s] Raw data (loadavg): 1.10 1.00 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4204 0 0 0 82941 37 0 0 25 0 1 0 1842458522 17895424 4191 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4369 4191 145 145 0 4224 0 [pid=26658] vsize: 17476 Current children cumulated CPU time (s) 829.79 Current children cumulated vsize (Kb) 19600 [startup+840.072 s] Raw data (loadavg): 1.09 1.00 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4222 0 0 0 83941 37 0 0 25 0 1 0 1842458522 17993728 4209 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4393 4209 145 145 0 4248 0 [pid=26658] vsize: 17572 Current children cumulated CPU time (s) 839.79 Current children cumulated vsize (Kb) 19696 [startup+850.073 s] Raw data (loadavg): 1.15 1.02 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4229 0 0 0 84941 37 0 0 25 0 1 0 1842458522 18026496 4216 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4401 4216 145 145 0 4256 0 [pid=26658] vsize: 17604 Current children cumulated CPU time (s) 849.79 Current children cumulated vsize (Kb) 19728 [startup+860.074 s] Raw data (loadavg): 1.13 1.02 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4299 0 0 0 85940 37 0 0 25 0 1 0 1842458522 18325504 4286 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4474 4286 145 145 0 4329 0 [pid=26658] vsize: 17896 Current children cumulated CPU time (s) 859.78 Current children cumulated vsize (Kb) 20020 [startup+870.075 s] Raw data (loadavg): 1.11 1.02 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4643 0 0 0 86936 39 0 0 25 0 1 0 1842458522 19755008 4630 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4823 4630 145 145 0 4678 0 [pid=26658] vsize: 19292 Current children cumulated CPU time (s) 869.76 Current children cumulated vsize (Kb) 21416 [startup+880.076 s] Raw data (loadavg): 1.09 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4668 0 0 0 87936 39 0 0 25 0 1 0 1842458522 19857408 4655 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4848 4655 145 145 0 4703 0 [pid=26658] vsize: 19392 Current children cumulated CPU time (s) 879.76 Current children cumulated vsize (Kb) 21516 [startup+890.077 s] Raw data (loadavg): 1.08 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4723 0 0 0 88935 40 0 0 25 0 1 0 1842458522 20090880 4710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4905 4710 145 145 0 4760 0 [pid=26658] vsize: 19620 Current children cumulated CPU time (s) 889.76 Current children cumulated vsize (Kb) 21744 [startup+900.078 s] Raw data (loadavg): 1.06 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4723 0 0 0 89935 40 0 0 25 0 1 0 1842458522 20090880 4710 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4905 4710 145 145 0 4760 0 [pid=26658] vsize: 19620 Current children cumulated CPU time (s) 899.76 Current children cumulated vsize (Kb) 21744 [startup+910.079 s] Raw data (loadavg): 1.05 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 90935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0 [pid=26658] vsize: 19620 Current children cumulated CPU time (s) 909.76 Current children cumulated vsize (Kb) 21744 [startup+920.079 s] Raw data (loadavg): 1.05 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 91935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0 [pid=26658] vsize: 19620 Current children cumulated CPU time (s) 919.76 Current children cumulated vsize (Kb) 21744 [startup+930.08 s] Raw data (loadavg): 1.04 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4724 0 0 0 92935 40 0 0 25 0 1 0 1842458522 20090880 4711 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 4905 4711 145 145 0 4760 0 [pid=26658] vsize: 19620 Current children cumulated CPU time (s) 929.76 Current children cumulated vsize (Kb) 21744 [startup+940.081 s] Raw data (loadavg): 1.03 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4850 0 0 0 93934 41 0 0 25 0 1 0 1842458522 20602880 4837 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5030 4837 145 145 0 4885 0 [pid=26658] vsize: 20120 Current children cumulated CPU time (s) 939.76 Current children cumulated vsize (Kb) 22244 [startup+950.082 s] Raw data (loadavg): 1.03 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4892 0 0 0 94933 42 0 0 25 0 1 0 1842458522 20774912 4879 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5072 4879 145 145 0 4927 0 [pid=26658] vsize: 20288 Current children cumulated CPU time (s) 949.76 Current children cumulated vsize (Kb) 22412 [startup+960.083 s] Raw data (loadavg): 1.02 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 95932 42 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 959.75 Current children cumulated vsize (Kb) 22528 [startup+970.084 s] Raw data (loadavg): 1.02 1.01 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 96932 43 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 969.76 Current children cumulated vsize (Kb) 22528 [startup+980.086 s] Raw data (loadavg): 1.02 1.00 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 97932 43 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 979.76 Current children cumulated vsize (Kb) 22528 [startup+990.086 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 98931 44 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 989.76 Current children cumulated vsize (Kb) 22528 [startup+1000.09 s] Raw data (loadavg): 1.09 1.02 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 99930 44 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 999.75 Current children cumulated vsize (Kb) 22528 [startup+1010.09 s] Raw data (loadavg): 1.08 1.02 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 100930 45 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1009.76 Current children cumulated vsize (Kb) 22528 [startup+1020.09 s] Raw data (loadavg): 1.06 1.02 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4916 0 0 0 101930 45 0 0 25 0 1 0 1842458522 20893696 4903 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4903 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1019.76 Current children cumulated vsize (Kb) 22528 [startup+1030.09 s] Raw data (loadavg): 1.05 1.02 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 102930 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1029.77 Current children cumulated vsize (Kb) 22528 [startup+1040.09 s] Raw data (loadavg): 1.04 1.02 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 103929 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1039.76 Current children cumulated vsize (Kb) 22528 [startup+1050.1 s] Raw data (loadavg): 1.04 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 104929 46 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1049.76 Current children cumulated vsize (Kb) 22528 [startup+1060.1 s] Raw data (loadavg): 1.03 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 105929 47 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1059.77 Current children cumulated vsize (Kb) 22528 [startup+1070.1 s] Raw data (loadavg): 1.03 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4917 0 0 0 106929 47 0 0 25 0 1 0 1842458522 20893696 4904 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4904 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1069.77 Current children cumulated vsize (Kb) 22528 [startup+1080.1 s] Raw data (loadavg): 1.02 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4918 0 0 0 107928 47 0 0 25 0 1 0 1842458522 20893696 4905 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4905 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1079.76 Current children cumulated vsize (Kb) 22528 [startup+1090.1 s] Raw data (loadavg): 1.02 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4918 0 0 0 108928 47 0 0 25 0 1 0 1842458522 20893696 4905 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4905 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1089.76 Current children cumulated vsize (Kb) 22528 [startup+1100.1 s] Raw data (loadavg): 1.01 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 109928 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1099.77 Current children cumulated vsize (Kb) 22528 [startup+1110.1 s] Raw data (loadavg): 1.01 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 110928 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1109.77 Current children cumulated vsize (Kb) 22528 [startup+1120.1 s] Raw data (loadavg): 1.01 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 111927 48 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1119.76 Current children cumulated vsize (Kb) 22528 [startup+1130.11 s] Raw data (loadavg): 1.01 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 112927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1129.77 Current children cumulated vsize (Kb) 22528 [startup+1140.11 s] Raw data (loadavg): 1.01 1.01 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 113927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1139.77 Current children cumulated vsize (Kb) 22528 [startup+1150.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 114927 49 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1149.77 Current children cumulated vsize (Kb) 22528 [startup+1160.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 115926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1159.77 Current children cumulated vsize (Kb) 22528 [startup+1170.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 116926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1169.77 Current children cumulated vsize (Kb) 22528 [startup+1180.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 4920 0 0 0 117926 50 0 0 25 0 1 0 1842458522 20893696 4907 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 5101 4907 145 145 0 4956 0 [pid=26658] vsize: 20404 Current children cumulated CPU time (s) 1179.77 Current children cumulated vsize (Kb) 22528 [startup+1190.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5187 0 0 0 118923 52 0 0 25 0 1 0 1842458522 21987328 5174 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 5368 5174 145 145 0 5223 0 [pid=26658] vsize: 21472 Current children cumulated CPU time (s) 1189.76 Current children cumulated vsize (Kb) 23596 [startup+1200.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5261 0 0 0 119922 52 0 0 25 0 1 0 1842458522 22302720 5248 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 5445 5248 145 145 0 5300 0 [pid=26658] vsize: 21780 Current children cumulated CPU time (s) 1199.75 Current children cumulated vsize (Kb) 23904 [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5331 0 0 0 120922 53 0 0 25 0 1 0 1842458522 22589440 5318 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 5515 5318 145 145 0 5370 0 [pid=26658] vsize: 22060 Current children cumulated CPU time (s) 1209.76 Current children cumulated vsize (Kb) 24184 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 26658 Raw data (/proc/26654/stat): 26654 (minisat+_script) S 26653 26654 21452 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1842458517 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/26654/statm): 531 226 485 147 0 384 0 [pid=26654] vsize: 2124 Raw data (/proc/26658/stat): 26658 (minisat+_64-bit) R 26654 26654 21452 0 -1 0 5331 0 0 0 120922 53 0 0 25 0 1 0 1842458522 22589440 5318 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26658/statm): 5515 5318 145 145 0 5370 0 [pid=26658] vsize: 22060 Current children cumulated CPU time (s) 1209.76 Current children cumulated vsize (Kb) 24184 Sending SIGTERM to -26654 Sleeping 2 seconds One traced child (pid=26654) ended because it received signal 15 (SIGTERM) One traced child (pid=26658) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1209.77 CPU user time (s): 1209.22 CPU system time (s): 0.544917 CPU usage (%): 99.9703 Max. virtual memory (cumulated for all children) (Kb): 24184
ERROR: no interpretation found !