Name | submitted/aloul/FPGA_SAT05/normalized-fpga45_44_sat_pb.cnf.cr.opb |
MD5SUM | c501a04dd091dbe678ec2743021adc30 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
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 | 46 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 14.2518 |
Number of variables | 2970 |
Total number of constraints | 2113 |
Number of constraints which are clauses | 2024 |
Number of constraints which are cardinality constraints (but not clauses) | 89 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 22 |
Maximum length of a constraint | 45 |
LAUNCH ON wulflinc22 THE 2005-09-18 12:37:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2395 boxname=wulflinc22 idbench=51 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c501a04dd091dbe678ec2743021adc30 /oldhome/oroussel/tmp/wulflinc22/normalized-fpga45_44_sat_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc22/normalized-fpga45_44_sat_pb.cnf.cr.opb IDLAUNCH: 2395 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.031 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 942808 kB Buffers: 33412 kB Cached: 31060 kB SwapCached: 536 kB Active: 53784 kB Inactive: 13252 kB HighTotal: 131008 kB HighFree: 97860 kB LowTotal: 903652 kB LowFree: 844948 kB SwapTotal: 2097892 kB SwapFree: 2096832 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5856 kB Slab: 19216 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:57:11 (client local time) WITH STATUS 0 IN 1208.42 SECONDS stats: 2395 7 1208.42 0
c Parsing PB file... c Converting 2113 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ---[ 88]---> BDD-cost: 85 c ---[ 87]---> BDD-cost: 85 c ---[ 86]---> BDD-cost: 85 c ---[ 85]---> BDD-cost: 85 c ---[ 84]---> BDD-cost: 85 c ---[ 83]---> BDD-cost: 85 c ---[ 82]---> BDD-cost: 85 c ---[ 81]---> BDD-cost: 85 c ---[ 80]---> BDD-cost: 85 c ---[ 79]---> BDD-cost: 85 c ---[ 78]---> BDD-cost: 85 c ---[ 77]---> BDD-cost: 85 c ---[ 76]---> BDD-cost: 85 c ---[ 75]---> BDD-cost: 85 c ---[ 74]---> BDD-cost: 85 c ---[ 73]---> BDD-cost: 85 c ---[ 72]---> BDD-cost: 85 c ---[ 71]---> BDD-cost: 85 c ---[ 70]---> BDD-cost: 85 c ---[ 69]---> BDD-cost: 85 c ---[ 68]---> BDD-cost: 85 c ---[ 67]---> BDD-cost: 85 c ---[ 66]---> BDD-cost: 85 c ---[ 65]---> BDD-cost: 85 c ---[ 64]---> BDD-cost: 85 c ---[ 63]---> BDD-cost: 85 c ---[ 62]---> BDD-cost: 85 c ---[ 61]---> BDD-cost: 85 c ---[ 60]---> BDD-cost: 85 c ---[ 59]---> BDD-cost: 85 c ---[ 58]---> BDD-cost: 85 c ---[ 57]---> BDD-cost: 85 c ---[ 56]---> BDD-cost: 85 c ---[ 55]---> BDD-cost: 85 c ---[ 54]---> BDD-cost: 85 c ---[ 53]---> BDD-cost: 85 c ---[ 52]---> BDD-cost: 85 c ---[ 51]---> BDD-cost: 85 c ---[ 50]---> BDD-cost: 85 c ---[ 49]---> BDD-cost: 85 c ---[ 48]---> BDD-cost: 85 c ---[ 47]---> BDD-cost: 85 c ---[ 46]---> BDD-cost: 85 c ---[ 45]---> BDD-cost: 85 c ---[ 44]---> BDD-cost: 85 c ---[ 43]---> BDD-cost: 41 c ---[ 42]---> BDD-cost: 41 c ---[ 41]---> BDD-cost: 41 c ---[ 40]---> BDD-cost: 41 c ---[ 39]---> BDD-cost: 41 c ---[ 38]---> BDD-cost: 41 c ---[ 37]---> BDD-cost: 41 c ---[ 36]---> BDD-cost: 41 c ---[ 35]---> BDD-cost: 41 c ---[ 34]---> BDD-cost: 41 c ---[ 33]---> BDD-cost: 41 c ---[ 32]---> BDD-cost: 41 c ---[ 31]---> BDD-cost: 41 c ---[ 30]---> BDD-cost: 41 c ---[ 29]---> BDD-cost: 41 c ---[ 28]---> BDD-cost: 41 c ---[ 27]---> BDD-cost: 41 c ---[ 26]---> BDD-cost: 41 c ---[ 25]---> BDD-cost: 41 c ---[ 24]---> BDD-cost: 41 c ---[ 23]---> BDD-cost: 41 c ---[ 22]---> BDD-cost: 41 c ---[ 21]---> BDD-cost: 43 c ---[ 20]---> BDD-cost: 43 c ---[ 19]---> BDD-cost: 43 c ---[ 18]---> BDD-cost: 43 c ---[ 17]---> BDD-cost: 43 c ---[ 16]---> BDD-cost: 43 c ---[ 15]---> BDD-cost: 43 c ---[ 14]---> BDD-cost: 43 c ---[ 13]---> BDD-cost: 43 c ---[ 12]---> BDD-cost: 43 c ---[ 11]---> BDD-cost: 43 c ---[ 10]---> BDD-cost: 43 c ---[ 9]---> BDD-cost: 43 c ---[ 8]---> BDD-cost: 43 c ---[ 7]---> BDD-cost: 43 c ---[ 6]---> BDD-cost: 43 c ---[ 5]---> BDD-cost: 43 c ---[ 4]---> BDD-cost: 43 c ---[ 3]---> BDD-cost: 43 c ---[ 2]---> BDD-cost: 43 c ---[ 1]---> BDD-cost: 43 c ---[ 0]---> BDD-cost: 43 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 16073 84083 | 5357 0 0 nan | 0.000 % | c | 101 | 16073 84083 | 5892 101 25615 253.6 | 1.030 % | c | 252 | 16073 84083 | 6481 252 61496 244.0 | 1.030 % | c | 477 | 16073 84083 | 7130 477 112639 236.1 | 1.030 % | c | 816 | 16073 84083 | 7843 816 210746 258.3 | 1.030 % | c | 1323 | 16073 84083 | 8627 1323 346348 261.8 | 1.030 % | c | 2083 | 16073 84083 | 9490 2083 564649 271.1 | 1.030 % | c | 3223 | 16073 84083 | 10439 3223 718568 223.0 | 1.030 % | c | 4931 | 16073 84083 | 11483 4931 1368853 277.6 | 1.030 % | c | 7493 | 16073 84083 | 12631 7493 2490469 332.4 | 1.030 % | c | 11338 | 16073 84083 | 13894 11338 3675913 324.2 | 1.030 % | c | 17111 | 16073 84083 | 15284 17111 5830865 340.8 | 1.030 % | c | 25761 | 16073 84083 | 16812 17206 6458966 375.4 | 1.030 % | c | 38737 | 16073 84083 | 18493 11018 2215373 201.1 | 1.030 % | c | 58201 | 16073 84083 | 20343 17865 7499448 419.8 | 1.030 % | c | 87396 | 16073 84083 | 22377 17045 3155458 185.1 | 1.030 % | c | 131187 | 16073 84083 | 24615 16857 8064521 478.4 | 1.030 % | c | 196875 | 16073 84083 | 27076 16816 7876802 468.4 | 1.030 % |
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/24000/stat): 24000 (minisat+_script) R 23999 24000 21452 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841308164 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24000/statm): 174 3 169 147 0 27 0 [pid=24000] 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=24001 New process pid=24002 New process pid=24003 execve syscall for /bin/sed executable One traced child (pid=24002) 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=24003) exited with status: 0 One traced child (pid=24001) exited with status: 0 New process pid=24004 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc22/normalized-fpga45_44_sat_pb.cnf.cr.opb [startup+10.005 s] Raw data (loadavg): 0.94 0.98 0.95 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 2860 0 3 0 949 13 0 0 25 0 1 0 1841308170 12001280 2849 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 2930 2849 145 145 0 2785 0 [pid=24004] vsize: 11720 Current children cumulated CPU time (s) 9.64 Current children cumulated vsize (Kb) 13844 [startup+20.0058 s] Raw data (loadavg): 0.95 0.98 0.95 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 4529 0 3 0 1928 24 0 0 25 0 1 0 1841308170 18853888 4518 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 4603 4518 145 145 0 4458 0 [pid=24004] vsize: 18412 Current children cumulated CPU time (s) 19.54 Current children cumulated vsize (Kb) 20536 [startup+30.0074 s] Raw data (loadavg): 0.95 0.98 0.95 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 5924 0 3 0 2906 32 0 0 25 0 1 0 1841308170 24559616 5913 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 5996 5913 145 145 0 5851 0 [pid=24004] vsize: 23984 Current children cumulated CPU time (s) 29.4 Current children cumulated vsize (Kb) 26108 [startup+40.0082 s] Raw data (loadavg): 1.03 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7035 0 3 0 3890 39 0 0 25 0 1 0 1841308170 29188096 7024 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7126 7024 145 145 0 6981 0 [pid=24004] vsize: 28504 Current children cumulated CPU time (s) 39.31 Current children cumulated vsize (Kb) 30628 [startup+50.0089 s] Raw data (loadavg): 1.03 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7104 0 3 0 4889 40 0 0 25 0 1 0 1841308170 29470720 7093 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7195 7093 145 145 0 7050 0 [pid=24004] vsize: 28780 Current children cumulated CPU time (s) 49.31 Current children cumulated vsize (Kb) 30904 [startup+60.0096 s] Raw data (loadavg): 1.02 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7104 0 3 0 5890 40 0 0 25 0 1 0 1841308170 29470720 7093 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7195 7093 145 145 0 7050 0 [pid=24004] vsize: 28780 Current children cumulated CPU time (s) 59.32 Current children cumulated vsize (Kb) 30904 [startup+70.0103 s] Raw data (loadavg): 1.02 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7890 0 3 0 6878 44 0 0 25 0 1 0 1841308170 32702464 7879 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 7984 7879 145 145 0 7839 0 [pid=24004] vsize: 31936 Current children cumulated CPU time (s) 69.24 Current children cumulated vsize (Kb) 34060 [startup+80.012 s] Raw data (loadavg): 1.02 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7893 0 3 0 7878 44 0 0 25 0 1 0 1841308170 32702464 7882 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7984 7882 145 145 0 7839 0 [pid=24004] vsize: 31936 Current children cumulated CPU time (s) 79.24 Current children cumulated vsize (Kb) 34060 [startup+90.0127 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 8878 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0 [pid=24004] vsize: 31936 Current children cumulated CPU time (s) 89.24 Current children cumulated vsize (Kb) 34060 [startup+100.013 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 9878 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0 [pid=24004] vsize: 31936 Current children cumulated CPU time (s) 99.24 Current children cumulated vsize (Kb) 34060 [startup+110.015 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 7894 0 3 0 10879 44 0 0 25 0 1 0 1841308170 32702464 7883 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 7984 7883 145 145 0 7839 0 [pid=24004] vsize: 31936 Current children cumulated CPU time (s) 109.25 Current children cumulated vsize (Kb) 34060 [startup+120.016 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 8144 0 3 0 11875 46 0 0 25 0 1 0 1841308170 33726464 8133 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 8234 8133 145 145 0 8089 0 [pid=24004] vsize: 32936 Current children cumulated CPU time (s) 119.23 Current children cumulated vsize (Kb) 35060 [startup+130.018 s] Raw data (loadavg): 1.01 1.00 0.96 1/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) T 24000 24000 21452 0 -1 0 8651 0 3 0 12868 49 0 0 25 0 1 0 1841308170 35815424 8640 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/24004/statm): 8744 8640 145 145 0 8599 0 [pid=24004] vsize: 34976 Current children cumulated CPU time (s) 129.19 Current children cumulated vsize (Kb) 37100 [startup+140.018 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9267 0 3 0 13858 53 0 0 25 0 1 0 1841308170 38354944 9256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 9364 9256 145 145 0 9219 0 [pid=24004] vsize: 37456 Current children cumulated CPU time (s) 139.13 Current children cumulated vsize (Kb) 39580 [startup+150.019 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9799 0 3 0 14851 56 0 0 25 0 1 0 1841308170 40542208 9788 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 9898 9788 145 145 0 9753 0 [pid=24004] vsize: 39592 Current children cumulated CPU time (s) 149.09 Current children cumulated vsize (Kb) 41716 [startup+160.021 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 15852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0 [pid=24004] vsize: 39592 Current children cumulated CPU time (s) 159.1 Current children cumulated vsize (Kb) 41716 [startup+170.021 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 16852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0 [pid=24004] vsize: 39592 Current children cumulated CPU time (s) 169.1 Current children cumulated vsize (Kb) 41716 [startup+180.022 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 17852 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223104 134556540 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0 [pid=24004] vsize: 39592 Current children cumulated CPU time (s) 179.1 Current children cumulated vsize (Kb) 41716 [startup+190.023 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 9800 0 3 0 18853 56 0 0 25 0 1 0 1841308170 40542208 9789 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 9898 9789 145 145 0 9753 0 [pid=24004] vsize: 39592 Current children cumulated CPU time (s) 189.11 Current children cumulated vsize (Kb) 41716 [startup+200.024 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 10594 0 3 0 19839 61 0 0 25 0 1 0 1841308170 43798528 10583 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 10693 10583 145 145 0 10548 0 [pid=24004] vsize: 42772 Current children cumulated CPU time (s) 199.02 Current children cumulated vsize (Kb) 44896 [startup+210.024 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 20818 69 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 208.89 Current children cumulated vsize (Kb) 50840 [startup+220.025 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 21817 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 218.89 Current children cumulated vsize (Kb) 50840 [startup+230.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 22818 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 228.9 Current children cumulated vsize (Kb) 50840 [startup+240.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12082 0 3 0 23818 70 0 0 25 0 1 0 1841308170 49885184 12071 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12071 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 238.9 Current children cumulated vsize (Kb) 50840 [startup+250.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 24818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 248.9 Current children cumulated vsize (Kb) 50840 [startup+260.029 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 25818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 258.9 Current children cumulated vsize (Kb) 50840 [startup+270.029 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 26818 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 268.9 Current children cumulated vsize (Kb) 50840 [startup+280.031 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 27819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 278.91 Current children cumulated vsize (Kb) 50840 [startup+290.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 28819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223056 134562146 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 288.91 Current children cumulated vsize (Kb) 50840 [startup+300.033 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 29819 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 298.91 Current children cumulated vsize (Kb) 50840 [startup+310.033 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 30820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 308.92 Current children cumulated vsize (Kb) 50840 [startup+320.034 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 31820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 318.92 Current children cumulated vsize (Kb) 50840 [startup+330.036 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 32820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 328.92 Current children cumulated vsize (Kb) 50840 [startup+340.036 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 33820 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 338.92 Current children cumulated vsize (Kb) 50840 [startup+350.037 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 34821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 348.93 Current children cumulated vsize (Kb) 50840 [startup+360.039 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 35821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 358.93 Current children cumulated vsize (Kb) 50840 [startup+370.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 36821 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 368.93 Current children cumulated vsize (Kb) 50840 [startup+380.041 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 37822 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 378.94 Current children cumulated vsize (Kb) 50840 [startup+390.042 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12083 0 3 0 38822 70 0 0 25 0 1 0 1841308170 49885184 12072 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12179 12072 145 145 0 12034 0 [pid=24004] vsize: 48716 Current children cumulated CPU time (s) 388.94 Current children cumulated vsize (Kb) 50840 [startup+400.043 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12275 0 3 0 39819 70 0 0 25 0 1 0 1841308170 50671616 12264 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 12371 12264 145 145 0 12226 0 [pid=24004] vsize: 49484 Current children cumulated CPU time (s) 398.91 Current children cumulated vsize (Kb) 51608 [startup+410.043 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 12976 0 3 0 40808 76 0 0 25 0 1 0 1841308170 53547008 12965 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 13073 12965 145 145 0 12928 0 [pid=24004] vsize: 52292 Current children cumulated CPU time (s) 408.86 Current children cumulated vsize (Kb) 54416 [startup+420.045 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13499 0 3 0 41801 78 0 0 25 0 1 0 1841308170 55701504 13488 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 13599 13488 145 145 0 13454 0 [pid=24004] vsize: 54396 Current children cumulated CPU time (s) 418.81 Current children cumulated vsize (Kb) 56520 [startup+430.047 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13675 0 3 0 42798 79 0 0 25 0 1 0 1841308170 56475648 13664 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 13788 13664 145 145 0 13643 0 [pid=24004] vsize: 55152 Current children cumulated CPU time (s) 428.79 Current children cumulated vsize (Kb) 57276 [startup+440.048 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 13898 0 3 0 43795 80 0 0 25 0 1 0 1841308170 57462784 13887 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14029 13887 145 145 0 13884 0 [pid=24004] vsize: 56116 Current children cumulated CPU time (s) 438.77 Current children cumulated vsize (Kb) 58240 [startup+450.048 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14387 0 3 0 44787 83 0 0 25 0 1 0 1841308170 59469824 14376 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14519 14376 145 145 0 14374 0 [pid=24004] vsize: 58076 Current children cumulated CPU time (s) 448.72 Current children cumulated vsize (Kb) 60200 [startup+460.049 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 45778 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134551454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 458.67 Current children cumulated vsize (Kb) 61872 [startup+470.05 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 46779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 468.68 Current children cumulated vsize (Kb) 61872 [startup+480.05 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 47779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 478.68 Current children cumulated vsize (Kb) 61872 [startup+490.051 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 48779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 488.68 Current children cumulated vsize (Kb) 61872 [startup+500.051 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 49779 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 498.68 Current children cumulated vsize (Kb) 61872 [startup+510.052 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 50780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 508.69 Current children cumulated vsize (Kb) 61872 [startup+520.052 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 51780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 518.69 Current children cumulated vsize (Kb) 61872 [startup+530.052 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 52780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 528.69 Current children cumulated vsize (Kb) 61872 [startup+540.053 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14805 0 3 0 53780 87 0 0 25 0 1 0 1841308170 61181952 14794 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 14937 14794 145 145 0 14792 0 [pid=24004] vsize: 59748 Current children cumulated CPU time (s) 538.69 Current children cumulated vsize (Kb) 61872 [startup+550.053 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 14874 0 3 0 54780 88 0 0 25 0 1 0 1841308170 61464576 14863 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 15006 14863 145 145 0 14861 0 [pid=24004] vsize: 60024 Current children cumulated CPU time (s) 548.7 Current children cumulated vsize (Kb) 62148 [startup+560.054 s] Raw data (loadavg): 1.07 1.02 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 15389 0 3 0 55772 90 0 0 25 0 1 0 1841308170 63586304 15378 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 15524 15378 145 145 0 15379 0 [pid=24004] vsize: 62096 Current children cumulated CPU time (s) 558.64 Current children cumulated vsize (Kb) 64220 [startup+570.055 s] Raw data (loadavg): 1.06 1.02 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 15879 0 3 0 56765 94 0 0 25 0 1 0 1841308170 65593344 15868 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16014 15868 145 145 0 15869 0 [pid=24004] vsize: 64056 Current children cumulated CPU time (s) 568.61 Current children cumulated vsize (Kb) 66180 [startup+580.056 s] Raw data (loadavg): 1.05 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16220 0 3 0 57760 96 0 0 25 0 1 0 1841308170 67002368 16209 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16358 16209 145 145 0 16213 0 [pid=24004] vsize: 65432 Current children cumulated CPU time (s) 578.58 Current children cumulated vsize (Kb) 67556 [startup+590.056 s] Raw data (loadavg): 1.04 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 58756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 588.55 Current children cumulated vsize (Kb) 68504 [startup+600.057 s] Raw data (loadavg): 1.04 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 59756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 598.55 Current children cumulated vsize (Kb) 68504 [startup+610.058 s] Raw data (loadavg): 1.03 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 60756 97 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 608.55 Current children cumulated vsize (Kb) 68504 [startup+620.058 s] Raw data (loadavg): 1.02 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 61756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 618.56 Current children cumulated vsize (Kb) 68504 [startup+630.059 s] Raw data (loadavg): 1.02 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 62756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223024 134556987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 628.56 Current children cumulated vsize (Kb) 68504 [startup+640.06 s] Raw data (loadavg): 1.02 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16455 0 3 0 63756 98 0 0 25 0 1 0 1841308170 67973120 16444 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16595 16444 145 145 0 16450 0 [pid=24004] vsize: 66380 Current children cumulated CPU time (s) 638.56 Current children cumulated vsize (Kb) 68504 [startup+650.059 s] Raw data (loadavg): 1.01 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 16642 0 3 0 64754 99 0 0 25 0 1 0 1841308170 68734976 16631 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 16781 16631 145 145 0 16636 0 [pid=24004] vsize: 67124 Current children cumulated CPU time (s) 648.55 Current children cumulated vsize (Kb) 69248 [startup+660.061 s] Raw data (loadavg): 1.01 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17491 0 3 0 65742 104 0 0 25 0 1 0 1841308170 72228864 17480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 17634 17480 145 145 0 17489 0 [pid=24004] vsize: 70536 Current children cumulated CPU time (s) 658.48 Current children cumulated vsize (Kb) 72660 [startup+670.062 s] Raw data (loadavg): 1.01 1.01 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17883 0 3 0 66737 106 0 0 25 0 1 0 1841308170 73842688 17872 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17872 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 668.45 Current children cumulated vsize (Kb) 74236 [startup+680.062 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17885 0 3 0 67737 106 0 0 25 0 1 0 1841308170 73842688 17874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17874 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 678.45 Current children cumulated vsize (Kb) 74236 [startup+690.062 s] Raw data (loadavg): 1.01 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17885 0 3 0 68737 106 0 0 25 0 1 0 1841308170 73842688 17874 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17874 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 688.45 Current children cumulated vsize (Kb) 74236 [startup+700.063 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 69738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 698.46 Current children cumulated vsize (Kb) 74236 [startup+710.064 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 70738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 708.46 Current children cumulated vsize (Kb) 74236 [startup+720.064 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 71738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 718.46 Current children cumulated vsize (Kb) 74236 [startup+730.065 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 72738 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 728.46 Current children cumulated vsize (Kb) 74236 [startup+740.066 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 73739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 738.47 Current children cumulated vsize (Kb) 74236 [startup+750.067 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 74739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 748.47 Current children cumulated vsize (Kb) 74236 [startup+760.068 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 75739 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 758.47 Current children cumulated vsize (Kb) 74236 [startup+770.069 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 76740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 768.48 Current children cumulated vsize (Kb) 74236 [startup+780.07 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 77740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 778.48 Current children cumulated vsize (Kb) 74236 [startup+790.071 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 78740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 788.48 Current children cumulated vsize (Kb) 74236 [startup+800.07 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 17886 0 3 0 79740 106 0 0 25 0 1 0 1841308170 73842688 17875 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18028 17875 145 145 0 17883 0 [pid=24004] vsize: 72112 Current children cumulated CPU time (s) 798.48 Current children cumulated vsize (Kb) 74236 [startup+810.071 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) T 24000 24000 21452 0 -1 0 18221 0 3 0 80735 108 0 0 25 0 1 0 1841308170 75264000 18210 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18375 18210 145 145 0 18230 0 [pid=24004] vsize: 73500 Current children cumulated CPU time (s) 808.45 Current children cumulated vsize (Kb) 75624 [startup+820.072 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 18819 0 3 0 81725 112 0 0 25 0 1 0 1841308170 77721600 18808 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 18975 18808 145 145 0 18830 0 [pid=24004] vsize: 75900 Current children cumulated CPU time (s) 818.39 Current children cumulated vsize (Kb) 78024 [startup+830.071 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19206 0 3 0 82720 114 0 0 25 0 1 0 1841308170 79388672 19195 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19382 19195 145 145 0 19237 0 [pid=24004] vsize: 77528 Current children cumulated CPU time (s) 828.36 Current children cumulated vsize (Kb) 79652 [startup+840.072 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 83716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 838.34 Current children cumulated vsize (Kb) 80800 [startup+850.073 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 84716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 848.34 Current children cumulated vsize (Kb) 80800 [startup+860.073 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 85716 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 858.34 Current children cumulated vsize (Kb) 80800 [startup+870.074 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 86717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 868.35 Current children cumulated vsize (Kb) 80800 [startup+880.075 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 87717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 878.35 Current children cumulated vsize (Kb) 80800 [startup+890.076 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 88717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 888.35 Current children cumulated vsize (Kb) 80800 [startup+900.076 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 89717 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 898.35 Current children cumulated vsize (Kb) 80800 [startup+910.077 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 90718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 908.36 Current children cumulated vsize (Kb) 80800 [startup+920.078 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 91718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 918.36 Current children cumulated vsize (Kb) 80800 [startup+930.078 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 92718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 928.36 Current children cumulated vsize (Kb) 80800 [startup+940.079 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19494 0 3 0 93718 116 0 0 25 0 1 0 1841308170 80564224 19483 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19483 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 938.36 Current children cumulated vsize (Kb) 80800 [startup+950.08 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 94719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 948.37 Current children cumulated vsize (Kb) 80800 [startup+960.082 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 95719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 958.37 Current children cumulated vsize (Kb) 80800 [startup+970.082 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 96719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 968.37 Current children cumulated vsize (Kb) 80800 [startup+980.083 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 97719 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 978.37 Current children cumulated vsize (Kb) 80800 [startup+990.084 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 98720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 988.38 Current children cumulated vsize (Kb) 80800 [startup+1000.08 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 99720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134556884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 998.38 Current children cumulated vsize (Kb) 80800 [startup+1010.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 100720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1008.38 Current children cumulated vsize (Kb) 80800 [startup+1020.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 101720 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1018.38 Current children cumulated vsize (Kb) 80800 [startup+1030.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 102721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1028.39 Current children cumulated vsize (Kb) 80800 [startup+1040.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 103721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1038.39 Current children cumulated vsize (Kb) 80800 [startup+1050.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 104721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1048.39 Current children cumulated vsize (Kb) 80800 [startup+1060.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 105721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1058.39 Current children cumulated vsize (Kb) 80800 [startup+1070.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 106721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1068.39 Current children cumulated vsize (Kb) 80800 [startup+1080.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 107722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1078.4 Current children cumulated vsize (Kb) 80800 [startup+1090.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 108722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1088.4 Current children cumulated vsize (Kb) 80800 [startup+1100.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 109721 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1098.39 Current children cumulated vsize (Kb) 80800 [startup+1110.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 110722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1108.4 Current children cumulated vsize (Kb) 80800 [startup+1120.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 111722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1118.4 Current children cumulated vsize (Kb) 80800 [startup+1130.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 112722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1128.4 Current children cumulated vsize (Kb) 80800 [startup+1140.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19497 0 3 0 113722 116 0 0 25 0 1 0 1841308170 80564224 19486 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19486 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1138.4 Current children cumulated vsize (Kb) 80800 [startup+1150.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19498 0 3 0 114723 116 0 0 25 0 1 0 1841308170 80564224 19487 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19487 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1148.41 Current children cumulated vsize (Kb) 80800 [startup+1160.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19499 0 3 0 115723 116 0 0 25 0 1 0 1841308170 80564224 19488 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 19669 19488 145 145 0 19524 0 [pid=24004] vsize: 78676 Current children cumulated CPU time (s) 1158.41 Current children cumulated vsize (Kb) 80800 [startup+1170.09 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 116717 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1168.38 Current children cumulated vsize (Kb) 82188 [startup+1180.1 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 117717 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1178.38 Current children cumulated vsize (Kb) 82188 [startup+1190.1 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 118718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1188.39 Current children cumulated vsize (Kb) 82188 [startup+1200.1 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 119718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1198.39 Current children cumulated vsize (Kb) 82188 [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 120718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1208.39 Current children cumulated vsize (Kb) 82188 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 1.00 1.00 0.96 2/57 24004 Raw data (/proc/24000/stat): 24000 (minisat+_script) S 23999 24000 21452 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1841308164 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24000/statm): 531 226 485 147 0 384 0 [pid=24000] vsize: 2124 Raw data (/proc/24004/stat): 24004 (minisat+_64-bit) R 24000 24000 21452 0 -1 0 19845 0 3 0 120718 119 0 0 25 0 1 0 1841308170 81985536 19834 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24004/statm): 20016 19834 145 145 0 19871 0 [pid=24004] vsize: 80064 Current children cumulated CPU time (s) 1208.39 Current children cumulated vsize (Kb) 82188 Sending SIGTERM to -24000 Sleeping 2 seconds One traced child (pid=24000) ended because it received signal 15 (SIGTERM) One traced child (pid=24004) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1208.42 CPU user time (s): 1207.19 CPU system time (s): 1.22981 CPU usage (%): 99.8576 Max. virtual memory (cumulated for all children) (Kb): 82188
ERROR: no interpretation found !