Name | submitted/aloul/FPGA_SAT05/normalized-chnl15_25_pb.cnf.cr.opb |
MD5SUM | 808390b13d2d87ec4e78f628ed3af9ba |
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 | 26 |
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.024995 |
Number of variables | 750 |
Total number of constraints | 80 |
Number of constraints which are clauses | 50 |
Number of constraints which are cardinality constraints (but not clauses) | 30 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 15 |
Maximum length of a constraint | 25 |
LAUNCH ON wulflinc7 THE 2005-09-18 12:23:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2349 boxname=wulflinc7 idbench=5 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 808390b13d2d87ec4e78f628ed3af9ba /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb IDLAUNCH: 2349 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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 : 2 cpu MHz : 451.050 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: 947156 kB Buffers: 34296 kB Cached: 28952 kB SwapCached: 740 kB Active: 54860 kB Inactive: 10948 kB HighTotal: 131008 kB HighFree: 99988 kB LowTotal: 903652 kB LowFree: 847168 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16012 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:44:04 (client local time) WITH STATUS 0 IN 1209.92 SECONDS stats: 2349 7 1209.92 0
c Parsing PB file... c Converting 80 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................. c ---[ 29]---> BDD-cost: 47 c ---[ 28]---> BDD-cost: 47 c ---[ 27]---> BDD-cost: 47 c ---[ 26]---> BDD-cost: 47 c ---[ 25]---> BDD-cost: 47 c ---[ 24]---> BDD-cost: 47 c ---[ 23]---> BDD-cost: 47 c ---[ 22]---> BDD-cost: 47 c ---[ 21]---> BDD-cost: 47 c ---[ 20]---> BDD-cost: 47 c ---[ 19]---> BDD-cost: 47 c ---[ 18]---> BDD-cost: 47 c ---[ 17]---> BDD-cost: 47 c ---[ 16]---> BDD-cost: 47 c ---[ 15]---> BDD-cost: 47 c ---[ 14]---> BDD-cost: 47 c ---[ 13]---> BDD-cost: 47 c ---[ 12]---> BDD-cost: 47 c ---[ 11]---> BDD-cost: 47 c ---[ 10]---> BDD-cost: 47 c ---[ 9]---> BDD-cost: 47 c ---[ 8]---> BDD-cost: 47 c ---[ 7]---> BDD-cost: 47 c ---[ 6]---> BDD-cost: 47 c ---[ 5]---> BDD-cost: 47 c ---[ 4]---> BDD-cost: 47 c ---[ 3]---> BDD-cost: 47 c ---[ 2]---> BDD-cost: 47 c ---[ 1]---> BDD-cost: 47 c ---[ 0]---> BDD-cost: 47 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 3530 9810 | 1176 0 0 nan | 0.000 % | c | 103 | 3530 9810 | 1293 103 5007 48.6 | 1.389 % | c | 253 | 3530 9810 | 1422 253 13026 51.5 | 1.389 % | c | 478 | 3530 9810 | 1565 478 27883 58.3 | 1.390 % | c | 818 | 3530 9810 | 1721 818 54244 66.3 | 1.389 % | c | 1324 | 3530 9810 | 1893 1324 89008 67.2 | 1.389 % | c | 2084 | 3530 9810 | 2083 2084 154915 74.3 | 1.389 % | c | 3224 | 3530 9810 | 2291 1835 146216 79.7 | 1.389 % | c | 4932 | 3530 9810 | 2520 2209 220568 99.8 | 1.389 % | c | 7494 | 3530 9810 | 2772 1902 214616 112.8 | 1.389 % | c | 11338 | 3530 9810 | 3050 2643 352193 133.3 | 1.389 % | c | 17107 | 3530 9810 | 3355 3014 336789 111.7 | 1.389 % | c | 25756 | 3530 9810 | 3690 2249 281918 125.4 | 1.389 % | c | 38731 | 3530 9810 | 4059 2796 359962 128.7 | 1.389 % | c | 58192 | 3530 9810 | 4465 2453 289039 117.8 | 1.389 % | c | 87386 | 3530 9810 | 4912 2518 277999 110.4 | 1.389 % | c | 131177 | 3530 9810 | 5403 3570 478640 134.1 | 1.389 % | c | 196861 | 3530 9810 | 5944 4748 630300 132.8 | 1.389 % | c | 295392 | 3530 9810 | 6538 4647 519495 111.8 | 1.389 % | c | 443181 | 3530 9810 | 7192 6344 768707 121.2 | 1.389 % | c | 664866 | 3530 9810 | 7911 7564 930517 123.0 | 1.389 % | c | 997394 | 3530 9810 | 8702 5038 677958 134.6 | 1.389 % |
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/17851/stat): 17851 (minisat+_script) R 17850 17851 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783025155 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/17851/statm): 174 3 169 147 0 27 0 [pid=17851] 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=17852 New process pid=17853 New process pid=17854 execve syscall for /bin/sed executable One traced child (pid=17853) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=17854) exited with status: 0 One traced child (pid=17852) exited with status: 0 New process pid=17855 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-chnl15_25_pb.cnf.cr.opb [startup+10.0049 s] Raw data (loadavg): 0.82 0.95 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 869 0 2 0 978 4 0 0 25 0 1 0 1783025160 3878912 858 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/17855/statm): 947 858 145 145 0 802 0 [pid=17855] vsize: 3788 Current children cumulated CPU time (s) 9.84 Current children cumulated vsize (Kb) 5912 [startup+20.0065 s] Raw data (loadavg): 0.85 0.95 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1037 0 2 0 1975 6 0 0 25 0 1 0 1783025160 4579328 1026 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1118 1026 145 145 0 973 0 [pid=17855] vsize: 4472 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 6596 [startup+30.0071 s] Raw data (loadavg): 0.87 0.95 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1181 0 2 0 2972 7 0 0 25 0 1 0 1783025160 5177344 1170 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/17855/statm): 1264 1170 145 145 0 1119 0 [pid=17855] vsize: 5056 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 7180 [startup+40.0088 s] Raw data (loadavg): 0.89 0.95 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1201 0 2 0 3971 7 0 0 25 0 1 0 1783025160 5259264 1190 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/17855/statm): 1284 1190 145 145 0 1139 0 [pid=17855] vsize: 5136 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 7260 [startup+50.0104 s] Raw data (loadavg): 0.91 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1251 0 2 0 4970 8 0 0 25 0 1 0 1783025160 5472256 1240 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1336 1240 145 145 0 1191 0 [pid=17855] vsize: 5344 Current children cumulated CPU time (s) 49.8 Current children cumulated vsize (Kb) 7468 [startup+60.011 s] Raw data (loadavg): 0.92 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1284 0 2 0 5970 9 0 0 25 0 1 0 1783025160 5615616 1273 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1371 1273 145 145 0 1226 0 [pid=17855] vsize: 5484 Current children cumulated CPU time (s) 59.81 Current children cumulated vsize (Kb) 7608 [startup+70.0126 s] Raw data (loadavg): 0.93 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1382 0 2 0 6969 9 0 0 25 0 1 0 1783025160 6033408 1371 4294967295 134512640 135094434 3221224432 3221223088 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1473 1371 145 145 0 1328 0 [pid=17855] vsize: 5892 Current children cumulated CPU time (s) 69.8 Current children cumulated vsize (Kb) 8016 [startup+80.0133 s] Raw data (loadavg): 0.94 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1468 0 2 0 7968 9 0 0 25 0 1 0 1783025160 6385664 1457 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1559 1457 145 145 0 1414 0 [pid=17855] vsize: 6236 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 8360 [startup+90.0139 s] Raw data (loadavg): 0.95 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1500 0 2 0 8967 10 0 0 25 0 1 0 1783025160 6516736 1489 4294967295 134512640 135094434 3221224432 3221223024 134556980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1591 1489 145 145 0 1446 0 [pid=17855] vsize: 6364 Current children cumulated CPU time (s) 89.79 Current children cumulated vsize (Kb) 8488 [startup+100.015 s] Raw data (loadavg): 0.96 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1508 0 2 0 9967 10 0 0 25 0 1 0 1783025160 6549504 1497 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1599 1497 145 145 0 1454 0 [pid=17855] vsize: 6396 Current children cumulated CPU time (s) 99.79 Current children cumulated vsize (Kb) 8520 [startup+110.015 s] Raw data (loadavg): 0.96 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1587 0 2 0 10967 11 0 0 25 0 1 0 1783025160 6868992 1576 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1677 1576 145 145 0 1532 0 [pid=17855] vsize: 6708 Current children cumulated CPU time (s) 109.8 Current children cumulated vsize (Kb) 8832 [startup+120.017 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1590 0 2 0 11967 11 0 0 25 0 1 0 1783025160 6881280 1579 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1680 1579 145 145 0 1535 0 [pid=17855] vsize: 6720 Current children cumulated CPU time (s) 119.8 Current children cumulated vsize (Kb) 8844 [startup+130.017 s] Raw data (loadavg): 0.97 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1590 0 2 0 12967 11 0 0 25 0 1 0 1783025160 6881280 1579 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1680 1579 145 145 0 1535 0 [pid=17855] vsize: 6720 Current children cumulated CPU time (s) 129.8 Current children cumulated vsize (Kb) 8844 [startup+140.018 s] Raw data (loadavg): 0.98 0.96 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1609 0 2 0 13967 11 0 0 25 0 1 0 1783025160 6963200 1598 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1700 1598 145 145 0 1555 0 [pid=17855] vsize: 6800 Current children cumulated CPU time (s) 139.8 Current children cumulated vsize (Kb) 8924 [startup+150.019 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1723 0 2 0 14966 12 0 0 25 0 1 0 1783025160 7442432 1712 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1817 1712 145 145 0 1672 0 [pid=17855] vsize: 7268 Current children cumulated CPU time (s) 149.8 Current children cumulated vsize (Kb) 9392 [startup+160.019 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1767 0 2 0 15966 12 0 0 25 0 1 0 1783025160 7643136 1756 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1866 1756 145 145 0 1721 0 [pid=17855] vsize: 7464 Current children cumulated CPU time (s) 159.8 Current children cumulated vsize (Kb) 9588 [startup+170.02 s] Raw data (loadavg): 0.98 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 16964 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0 [pid=17855] vsize: 7848 Current children cumulated CPU time (s) 169.79 Current children cumulated vsize (Kb) 9972 [startup+180.021 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 17963 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0 [pid=17855] vsize: 7848 Current children cumulated CPU time (s) 179.78 Current children cumulated vsize (Kb) 9972 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1860 0 2 0 18964 13 0 0 25 0 1 0 1783025160 8036352 1849 4294967295 134512640 135094434 3221224432 3221223088 134558113 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1962 1849 145 145 0 1817 0 [pid=17855] vsize: 7848 Current children cumulated CPU time (s) 189.79 Current children cumulated vsize (Kb) 9972 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1863 0 2 0 19964 13 0 0 25 0 1 0 1783025160 8048640 1852 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1965 1852 145 145 0 1820 0 [pid=17855] vsize: 7860 Current children cumulated CPU time (s) 199.79 Current children cumulated vsize (Kb) 9984 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1867 0 2 0 20964 13 0 0 25 0 1 0 1783025160 8065024 1856 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 1969 1856 145 145 0 1824 0 [pid=17855] vsize: 7876 Current children cumulated CPU time (s) 209.79 Current children cumulated vsize (Kb) 10000 [startup+220.024 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1924 0 2 0 21964 14 0 0 25 0 1 0 1783025160 8314880 1913 4294967295 134512640 135094434 3221224432 3221223024 134557419 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2030 1913 145 145 0 1885 0 [pid=17855] vsize: 8120 Current children cumulated CPU time (s) 219.8 Current children cumulated vsize (Kb) 10244 [startup+230.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1956 0 2 0 22964 14 0 0 25 0 1 0 1783025160 8437760 1945 4294967295 134512640 135094434 3221224432 3221223024 134557488 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2060 1945 145 145 0 1915 0 [pid=17855] vsize: 8240 Current children cumulated CPU time (s) 229.8 Current children cumulated vsize (Kb) 10364 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 1956 0 2 0 23964 14 0 0 25 0 1 0 1783025160 8437760 1945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2060 1945 145 145 0 1915 0 [pid=17855] vsize: 8240 Current children cumulated CPU time (s) 239.8 Current children cumulated vsize (Kb) 10364 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2032 0 2 0 24963 15 0 0 25 0 1 0 1783025160 8749056 2021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2136 2021 145 145 0 1991 0 [pid=17855] vsize: 8544 Current children cumulated CPU time (s) 249.8 Current children cumulated vsize (Kb) 10668 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2075 0 2 0 25963 15 0 0 25 0 1 0 1783025160 8925184 2064 4294967295 134512640 135094434 3221224432 3221223120 134554763 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2179 2064 145 145 0 2034 0 [pid=17855] vsize: 8716 Current children cumulated CPU time (s) 259.8 Current children cumulated vsize (Kb) 10840 [startup+270.028 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2075 0 2 0 26963 15 0 0 25 0 1 0 1783025160 8925184 2064 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2179 2064 145 145 0 2034 0 [pid=17855] vsize: 8716 Current children cumulated CPU time (s) 269.8 Current children cumulated vsize (Kb) 10840 [startup+280.029 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2102 0 2 0 27963 15 0 0 25 0 1 0 1783025160 9027584 2091 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2204 2091 145 145 0 2059 0 [pid=17855] vsize: 8816 Current children cumulated CPU time (s) 279.8 Current children cumulated vsize (Kb) 10940 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2130 0 2 0 28963 15 0 0 25 0 1 0 1783025160 9158656 2119 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2236 2119 145 145 0 2091 0 [pid=17855] vsize: 8944 Current children cumulated CPU time (s) 289.8 Current children cumulated vsize (Kb) 11068 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2135 0 2 0 29963 15 0 0 25 0 1 0 1783025160 9191424 2124 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2244 2124 145 145 0 2099 0 [pid=17855] vsize: 8976 Current children cumulated CPU time (s) 299.8 Current children cumulated vsize (Kb) 11100 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2154 0 2 0 30963 15 0 0 25 0 1 0 1783025160 9269248 2143 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2263 2143 145 145 0 2118 0 [pid=17855] vsize: 9052 Current children cumulated CPU time (s) 309.8 Current children cumulated vsize (Kb) 11176 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2159 0 2 0 31963 15 0 0 25 0 1 0 1783025160 9302016 2148 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2271 2148 145 145 0 2126 0 [pid=17855] vsize: 9084 Current children cumulated CPU time (s) 319.8 Current children cumulated vsize (Kb) 11208 [startup+330.033 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2159 0 2 0 32964 15 0 0 25 0 1 0 1783025160 9302016 2148 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2271 2148 145 145 0 2126 0 [pid=17855] vsize: 9084 Current children cumulated CPU time (s) 329.81 Current children cumulated vsize (Kb) 11208 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2219 0 2 0 33963 16 0 0 25 0 1 0 1783025160 9568256 2208 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2336 2208 145 145 0 2191 0 [pid=17855] vsize: 9344 Current children cumulated CPU time (s) 339.81 Current children cumulated vsize (Kb) 11468 [startup+350.035 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2223 0 2 0 34963 16 0 0 25 0 1 0 1783025160 9584640 2212 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2340 2212 145 145 0 2195 0 [pid=17855] vsize: 9360 Current children cumulated CPU time (s) 349.81 Current children cumulated vsize (Kb) 11484 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2249 0 2 0 35963 16 0 0 25 0 1 0 1783025160 9728000 2238 4294967295 134512640 135094434 3221224432 3221223104 134555890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2375 2238 145 145 0 2230 0 [pid=17855] vsize: 9500 Current children cumulated CPU time (s) 359.81 Current children cumulated vsize (Kb) 11624 [startup+370.038 s] Raw data (loadavg): 0.99 0.97 0.95 3/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2255 0 2 0 36964 16 0 0 25 0 1 0 1783025160 9740288 2244 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2378 2244 145 145 0 2233 0 [pid=17855] vsize: 9512 Current children cumulated CPU time (s) 369.82 Current children cumulated vsize (Kb) 11636 [startup+380.037 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2279 0 2 0 37963 16 0 0 25 0 1 0 1783025160 9850880 2268 4294967295 134512640 135094434 3221224432 3221223104 134556549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2405 2268 145 145 0 2260 0 [pid=17855] vsize: 9620 Current children cumulated CPU time (s) 379.81 Current children cumulated vsize (Kb) 11744 [startup+390.039 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2304 0 2 0 38963 16 0 0 25 0 1 0 1783025160 9981952 2293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2437 2293 145 145 0 2292 0 [pid=17855] vsize: 9748 Current children cumulated CPU time (s) 389.81 Current children cumulated vsize (Kb) 11872 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2321 0 2 0 39964 16 0 0 25 0 1 0 1783025160 10076160 2310 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2460 2310 145 145 0 2315 0 [pid=17855] vsize: 9840 Current children cumulated CPU time (s) 399.82 Current children cumulated vsize (Kb) 11964 [startup+410.04 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2438 0 2 0 40961 18 0 0 25 0 1 0 1783025160 10559488 2427 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2578 2427 145 145 0 2433 0 [pid=17855] vsize: 10312 Current children cumulated CPU time (s) 409.81 Current children cumulated vsize (Kb) 12436 [startup+420.042 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2535 0 2 0 41960 18 0 0 25 0 1 0 1783025160 10952704 2524 4294967295 134512640 135094434 3221224432 3221222992 134550333 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2674 2524 145 145 0 2529 0 [pid=17855] vsize: 10696 Current children cumulated CPU time (s) 419.8 Current children cumulated vsize (Kb) 12820 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2574 0 2 0 42960 19 0 0 25 0 1 0 1783025160 11141120 2563 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2720 2563 145 145 0 2575 0 [pid=17855] vsize: 10880 Current children cumulated CPU time (s) 429.81 Current children cumulated vsize (Kb) 13004 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2580 0 2 0 43960 19 0 0 25 0 1 0 1783025160 11169792 2569 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2727 2569 145 145 0 2582 0 [pid=17855] vsize: 10908 Current children cumulated CPU time (s) 439.81 Current children cumulated vsize (Kb) 13032 [startup+450.044 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2583 0 2 0 44960 19 0 0 25 0 1 0 1783025160 11169792 2572 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2727 2572 145 145 0 2582 0 [pid=17855] vsize: 10908 Current children cumulated CPU time (s) 449.81 Current children cumulated vsize (Kb) 13032 [startup+460.045 s] Raw data (loadavg): 0.99 0.97 0.95 3/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2603 0 2 0 45960 19 0 0 25 0 1 0 1783025160 11272192 2592 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2752 2592 145 145 0 2607 0 [pid=17855] vsize: 11008 Current children cumulated CPU time (s) 459.81 Current children cumulated vsize (Kb) 13132 [startup+470.045 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2608 0 2 0 46960 19 0 0 25 0 1 0 1783025160 11304960 2597 4294967295 134512640 135094434 3221224432 3221223024 134551925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2760 2597 145 145 0 2615 0 [pid=17855] vsize: 11040 Current children cumulated CPU time (s) 469.81 Current children cumulated vsize (Kb) 13164 [startup+480.046 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2613 0 2 0 47961 19 0 0 25 0 1 0 1783025160 11337728 2602 4294967295 134512640 135094434 3221224432 3221222188 134563367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2768 2602 145 145 0 2623 0 [pid=17855] vsize: 11072 Current children cumulated CPU time (s) 479.82 Current children cumulated vsize (Kb) 13196 [startup+490.047 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 48960 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0 [pid=17855] vsize: 11372 Current children cumulated CPU time (s) 489.81 Current children cumulated vsize (Kb) 13496 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 49961 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223024 134551997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0 [pid=17855] vsize: 11372 Current children cumulated CPU time (s) 499.82 Current children cumulated vsize (Kb) 13496 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2680 0 2 0 50961 19 0 0 25 0 1 0 1783025160 11644928 2669 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2843 2669 145 145 0 2698 0 [pid=17855] vsize: 11372 Current children cumulated CPU time (s) 509.82 Current children cumulated vsize (Kb) 13496 [startup+520.049 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2681 0 2 0 51961 19 0 0 25 0 1 0 1783025160 11644928 2670 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2843 2670 145 145 0 2698 0 [pid=17855] vsize: 11372 Current children cumulated CPU time (s) 519.82 Current children cumulated vsize (Kb) 13496 [startup+530.05 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 52961 19 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 529.82 Current children cumulated vsize (Kb) 13556 [startup+540.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 53961 19 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 539.82 Current children cumulated vsize (Kb) 13556 [startup+550.051 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 54961 20 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 549.83 Current children cumulated vsize (Kb) 13556 [startup+560.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 55960 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 559.83 Current children cumulated vsize (Kb) 13556 [startup+570.052 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 56961 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223056 134562051 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 569.84 Current children cumulated vsize (Kb) 13556 [startup+580.053 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2691 0 2 0 57961 21 0 0 25 0 1 0 1783025160 11706368 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2858 2680 145 145 0 2713 0 [pid=17855] vsize: 11432 Current children cumulated CPU time (s) 579.84 Current children cumulated vsize (Kb) 13556 [startup+590.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2697 0 2 0 58961 21 0 0 25 0 1 0 1783025160 11739136 2686 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2866 2686 145 145 0 2721 0 [pid=17855] vsize: 11464 Current children cumulated CPU time (s) 589.84 Current children cumulated vsize (Kb) 13588 [startup+600.054 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2709 0 2 0 59961 21 0 0 25 0 1 0 1783025160 11788288 2698 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2878 2698 145 145 0 2733 0 [pid=17855] vsize: 11512 Current children cumulated CPU time (s) 599.84 Current children cumulated vsize (Kb) 13636 [startup+610.055 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2711 0 2 0 60961 21 0 0 25 0 1 0 1783025160 11808768 2700 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2883 2700 145 145 0 2738 0 [pid=17855] vsize: 11532 Current children cumulated CPU time (s) 609.84 Current children cumulated vsize (Kb) 13656 [startup+620.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2711 0 2 0 61961 21 0 0 25 0 1 0 1783025160 11808768 2700 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2883 2700 145 145 0 2738 0 [pid=17855] vsize: 11532 Current children cumulated CPU time (s) 619.84 Current children cumulated vsize (Kb) 13656 [startup+630.056 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2721 0 2 0 62960 22 0 0 25 0 1 0 1783025160 11874304 2710 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 2899 2710 145 145 0 2754 0 [pid=17855] vsize: 11596 Current children cumulated CPU time (s) 629.84 Current children cumulated vsize (Kb) 13720 [startup+640.057 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2917 0 2 0 63959 22 0 0 25 0 1 0 1783025160 12709888 2906 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3103 2906 145 145 0 2958 0 [pid=17855] vsize: 12412 Current children cumulated CPU time (s) 639.83 Current children cumulated vsize (Kb) 14536 [startup+650.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2940 0 2 0 64959 22 0 0 25 0 1 0 1783025160 12804096 2929 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3126 2929 145 145 0 2981 0 [pid=17855] vsize: 12504 Current children cumulated CPU time (s) 649.83 Current children cumulated vsize (Kb) 14628 [startup+660.058 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2972 0 2 0 65958 22 0 0 25 0 1 0 1783025160 12959744 2961 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3164 2961 145 145 0 3019 0 [pid=17855] vsize: 12656 Current children cumulated CPU time (s) 659.82 Current children cumulated vsize (Kb) 14780 [startup+670.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2978 0 2 0 66958 22 0 0 25 0 1 0 1783025160 12992512 2967 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3172 2967 145 145 0 3027 0 [pid=17855] vsize: 12688 Current children cumulated CPU time (s) 669.82 Current children cumulated vsize (Kb) 14812 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2986 0 2 0 67959 22 0 0 25 0 1 0 1783025160 13025280 2975 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3180 2975 145 145 0 3035 0 [pid=17855] vsize: 12720 Current children cumulated CPU time (s) 679.83 Current children cumulated vsize (Kb) 14844 [startup+690.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 2991 0 2 0 68959 23 0 0 25 0 1 0 1783025160 13058048 2980 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3188 2980 145 145 0 3043 0 [pid=17855] vsize: 12752 Current children cumulated CPU time (s) 689.84 Current children cumulated vsize (Kb) 14876 [startup+700.062 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3009 0 2 0 69959 23 0 0 25 0 1 0 1783025160 13156352 2998 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3212 2998 145 145 0 3067 0 [pid=17855] vsize: 12848 Current children cumulated CPU time (s) 699.84 Current children cumulated vsize (Kb) 14972 [startup+710.061 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3009 0 2 0 70959 23 0 0 25 0 1 0 1783025160 13156352 2998 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3212 2998 145 145 0 3067 0 [pid=17855] vsize: 12848 Current children cumulated CPU time (s) 709.84 Current children cumulated vsize (Kb) 14972 [startup+720.063 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3021 0 2 0 71959 23 0 0 25 0 1 0 1783025160 13221888 3010 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3228 3010 145 145 0 3083 0 [pid=17855] vsize: 12912 Current children cumulated CPU time (s) 719.84 Current children cumulated vsize (Kb) 15036 [startup+730.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3029 0 2 0 72959 23 0 0 25 0 1 0 1783025160 13254656 3018 4294967295 134512640 135094434 3221224432 3221223104 134555579 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3236 3018 145 145 0 3091 0 [pid=17855] vsize: 12944 Current children cumulated CPU time (s) 729.84 Current children cumulated vsize (Kb) 15068 [startup+740.064 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3068 0 2 0 73959 23 0 0 25 0 1 0 1783025160 13406208 3057 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3273 3057 145 145 0 3128 0 [pid=17855] vsize: 13092 Current children cumulated CPU time (s) 739.84 Current children cumulated vsize (Kb) 15216 [startup+750.065 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3068 0 2 0 74959 23 0 0 25 0 1 0 1783025160 13406208 3057 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3273 3057 145 145 0 3128 0 [pid=17855] vsize: 13092 Current children cumulated CPU time (s) 749.84 Current children cumulated vsize (Kb) 15216 [startup+760.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3079 0 2 0 75959 23 0 0 25 0 1 0 1783025160 13471744 3068 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3289 3068 145 145 0 3144 0 [pid=17855] vsize: 13156 Current children cumulated CPU time (s) 759.84 Current children cumulated vsize (Kb) 15280 [startup+770.066 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3079 0 2 0 76959 24 0 0 25 0 1 0 1783025160 13471744 3068 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3289 3068 145 145 0 3144 0 [pid=17855] vsize: 13156 Current children cumulated CPU time (s) 769.85 Current children cumulated vsize (Kb) 15280 [startup+780.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3091 0 2 0 77959 24 0 0 25 0 1 0 1783025160 13520896 3080 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3301 3080 145 145 0 3156 0 [pid=17855] vsize: 13204 Current children cumulated CPU time (s) 779.85 Current children cumulated vsize (Kb) 15328 [startup+790.067 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3099 0 2 0 78959 24 0 0 25 0 1 0 1783025160 13570048 3088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3313 3088 145 145 0 3168 0 [pid=17855] vsize: 13252 Current children cumulated CPU time (s) 789.85 Current children cumulated vsize (Kb) 15376 [startup+800.068 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3124 0 2 0 79959 24 0 0 25 0 1 0 1783025160 13684736 3113 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3341 3113 145 145 0 3196 0 [pid=17855] vsize: 13364 Current children cumulated CPU time (s) 799.85 Current children cumulated vsize (Kb) 15488 [startup+810.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3143 0 2 0 80960 24 0 0 25 0 1 0 1783025160 13783040 3132 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3365 3132 145 145 0 3220 0 [pid=17855] vsize: 13460 Current children cumulated CPU time (s) 809.86 Current children cumulated vsize (Kb) 15584 [startup+820.069 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3143 0 2 0 81960 24 0 0 25 0 1 0 1783025160 13783040 3132 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3365 3132 145 145 0 3220 0 [pid=17855] vsize: 13460 Current children cumulated CPU time (s) 819.86 Current children cumulated vsize (Kb) 15584 [startup+830.07 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3165 0 2 0 82960 24 0 0 25 0 1 0 1783025160 13881344 3154 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3389 3154 145 145 0 3244 0 [pid=17855] vsize: 13556 Current children cumulated CPU time (s) 829.86 Current children cumulated vsize (Kb) 15680 [startup+840.072 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3165 0 2 0 83960 24 0 0 25 0 1 0 1783025160 13881344 3154 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3389 3154 145 145 0 3244 0 [pid=17855] vsize: 13556 Current children cumulated CPU time (s) 839.86 Current children cumulated vsize (Kb) 15680 [startup+850.072 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3210 0 2 0 84960 24 0 0 25 0 1 0 1783025160 14082048 3199 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3438 3199 145 145 0 3293 0 [pid=17855] vsize: 13752 Current children cumulated CPU time (s) 849.86 Current children cumulated vsize (Kb) 15876 [startup+860.072 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3266 0 2 0 85960 25 0 0 25 0 1 0 1783025160 14323712 3255 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3255 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 859.87 Current children cumulated vsize (Kb) 16112 [startup+870.073 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3268 0 2 0 86960 25 0 0 25 0 1 0 1783025160 14323712 3257 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3257 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 869.87 Current children cumulated vsize (Kb) 16112 [startup+880.074 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 87960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555666 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 879.87 Current children cumulated vsize (Kb) 16112 [startup+890.075 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 88960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 889.87 Current children cumulated vsize (Kb) 16112 [startup+900.075 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 89960 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 899.87 Current children cumulated vsize (Kb) 16112 [startup+910.076 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 90961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 909.88 Current children cumulated vsize (Kb) 16112 [startup+920.077 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 91961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 919.88 Current children cumulated vsize (Kb) 16112 [startup+930.077 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 92961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 929.88 Current children cumulated vsize (Kb) 16112 [startup+940.078 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 93961 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 939.88 Current children cumulated vsize (Kb) 16112 [startup+950.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 94962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 949.89 Current children cumulated vsize (Kb) 16112 [startup+960.079 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 95962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 959.89 Current children cumulated vsize (Kb) 16112 [startup+970.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 96962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 969.89 Current children cumulated vsize (Kb) 16112 [startup+980.081 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 97962 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 979.89 Current children cumulated vsize (Kb) 16112 [startup+990.082 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 98963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 989.9 Current children cumulated vsize (Kb) 16112 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 99963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 999.9 Current children cumulated vsize (Kb) 16112 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3271 0 2 0 100963 25 0 0 25 0 1 0 1783025160 14323712 3260 4294967295 134512640 135094434 3221224432 3221223104 134555300 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/17855/statm): 3497 3260 145 145 0 3352 0 [pid=17855] vsize: 13988 Current children cumulated CPU time (s) 1009.9 Current children cumulated vsize (Kb) 16112 [startup+1020.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3302 0 2 0 101962 26 0 0 25 0 1 0 1783025160 14446592 3291 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3527 3291 145 145 0 3382 0 [pid=17855] vsize: 14108 Current children cumulated CPU time (s) 1019.9 Current children cumulated vsize (Kb) 16232 [startup+1030.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3364 0 2 0 102961 26 0 0 25 0 1 0 1783025160 14749696 3353 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3601 3353 145 145 0 3456 0 [pid=17855] vsize: 14404 Current children cumulated CPU time (s) 1029.89 Current children cumulated vsize (Kb) 16528 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3376 0 2 0 103961 26 0 0 25 0 1 0 1783025160 14798848 3365 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3613 3365 145 145 0 3468 0 [pid=17855] vsize: 14452 Current children cumulated CPU time (s) 1039.89 Current children cumulated vsize (Kb) 16576 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 104961 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0 [pid=17855] vsize: 14484 Current children cumulated CPU time (s) 1049.89 Current children cumulated vsize (Kb) 16608 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 105962 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0 [pid=17855] vsize: 14484 Current children cumulated CPU time (s) 1059.9 Current children cumulated vsize (Kb) 16608 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3381 0 2 0 106962 26 0 0 25 0 1 0 1783025160 14831616 3370 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3621 3370 145 145 0 3476 0 [pid=17855] vsize: 14484 Current children cumulated CPU time (s) 1069.9 Current children cumulated vsize (Kb) 16608 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3382 0 2 0 107962 26 0 0 25 0 1 0 1783025160 14831616 3371 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3621 3371 145 145 0 3476 0 [pid=17855] vsize: 14484 Current children cumulated CPU time (s) 1079.9 Current children cumulated vsize (Kb) 16608 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3382 0 2 0 108962 26 0 0 25 0 1 0 1783025160 14831616 3371 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3621 3371 145 145 0 3476 0 [pid=17855] vsize: 14484 Current children cumulated CPU time (s) 1089.9 Current children cumulated vsize (Kb) 16608 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3425 0 2 0 109962 26 0 0 25 0 1 0 1783025160 15011840 3414 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3665 3414 145 145 0 3520 0 [pid=17855] vsize: 14660 Current children cumulated CPU time (s) 1099.9 Current children cumulated vsize (Kb) 16784 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 110962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0 [pid=17855] vsize: 14804 Current children cumulated CPU time (s) 1109.91 Current children cumulated vsize (Kb) 16928 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 111962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0 [pid=17855] vsize: 14804 Current children cumulated CPU time (s) 1119.91 Current children cumulated vsize (Kb) 16928 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 112962 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0 [pid=17855] vsize: 14804 Current children cumulated CPU time (s) 1129.91 Current children cumulated vsize (Kb) 16928 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3462 0 2 0 113963 27 0 0 25 0 1 0 1783025160 15159296 3451 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3701 3451 145 145 0 3556 0 [pid=17855] vsize: 14804 Current children cumulated CPU time (s) 1139.92 Current children cumulated vsize (Kb) 16928 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3463 0 2 0 114962 28 0 0 25 0 1 0 1783025160 15163392 3452 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3702 3452 145 145 0 3557 0 [pid=17855] vsize: 14808 Current children cumulated CPU time (s) 1149.92 Current children cumulated vsize (Kb) 16932 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3521 0 2 0 115960 29 0 0 25 0 1 0 1783025160 15400960 3510 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3760 3510 145 145 0 3615 0 [pid=17855] vsize: 15040 Current children cumulated CPU time (s) 1159.91 Current children cumulated vsize (Kb) 17164 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3532 0 2 0 116960 29 0 0 25 0 1 0 1783025160 15466496 3521 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3776 3521 145 145 0 3631 0 [pid=17855] vsize: 15104 Current children cumulated CPU time (s) 1169.91 Current children cumulated vsize (Kb) 17228 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.95 3/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3533 0 2 0 117961 29 0 0 25 0 1 0 1783025160 15470592 3522 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3777 3522 145 145 0 3632 0 [pid=17855] vsize: 15108 Current children cumulated CPU time (s) 1179.92 Current children cumulated vsize (Kb) 17232 [startup+1190.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3543 0 2 0 118961 29 0 0 25 0 1 0 1783025160 15532032 3532 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3792 3532 145 145 0 3647 0 [pid=17855] vsize: 15168 Current children cumulated CPU time (s) 1189.92 Current children cumulated vsize (Kb) 17292 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3565 0 2 0 119961 29 0 0 25 0 1 0 1783025160 15626240 3554 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3815 3554 145 145 0 3670 0 [pid=17855] vsize: 15260 Current children cumulated CPU time (s) 1199.92 Current children cumulated vsize (Kb) 17384 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3570 0 2 0 120961 30 0 0 25 0 1 0 1783025160 15659008 3559 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3823 3559 145 145 0 3678 0 [pid=17855] vsize: 15292 Current children cumulated CPU time (s) 1209.93 Current children cumulated vsize (Kb) 17416 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.95 2/57 17855 Raw data (/proc/17851/stat): 17851 (minisat+_script) S 17850 17851 15400 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1783025155 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/17851/statm): 531 226 485 147 0 384 0 [pid=17851] vsize: 2124 Raw data (/proc/17855/stat): 17855 (minisat+_64-bit) R 17851 17851 15400 0 -1 0 3570 0 2 0 120961 30 0 0 25 0 1 0 1783025160 15659008 3559 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/17855/statm): 3823 3559 145 145 0 3678 0 [pid=17855] vsize: 15292 Current children cumulated CPU time (s) 1209.93 Current children cumulated vsize (Kb) 17416 Sending SIGTERM to -17851 Sleeping 2 seconds One traced child (pid=17851) ended because it received signal 15 (SIGTERM) One traced child (pid=17855) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.11 CPU time (s): 1209.92 CPU user time (s): 1209.61 CPU system time (s): 0.308953 CPU usage (%): 99.9844 Max. virtual memory (cumulated for all children) (Kb): 17416
ERROR: no interpretation found !