Name | submitted/aloul/FPGA_SAT05/normalized-fpga40_40_sat_pb.cnf.cr.opb |
MD5SUM | f9a3a990ebca4aa5457d0675d3f1fe27 |
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 | 41 |
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 | 1.91671 |
Number of variables | 2400 |
Total number of constraints | 1720 |
Number of constraints which are clauses | 1640 |
Number of constraints which are cardinality constraints (but not clauses) | 80 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 40 |
LAUNCH ON wulflinc10 THE 2005-09-18 12:34:37 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2393 boxname=wulflinc10 idbench=49 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: f9a3a990ebca4aa5457d0675d3f1fe27 /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb IDLAUNCH: 2393 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 948020 kB Buffers: 34052 kB Cached: 25968 kB SwapCached: 228 kB Active: 54116 kB Inactive: 8872 kB HighTotal: 131008 kB HighFree: 101248 kB LowTotal: 903652 kB LowFree: 846772 kB SwapTotal: 2097136 kB SwapFree: 2096756 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6272 kB Slab: 18112 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:54:47 (client local time) WITH STATUS 0 IN 1208.36 SECONDS stats: 2393 7 1208.36 0
c Parsing PB file... c Converting 1720 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ---[ 79]---> BDD-cost: 77 c ---[ 78]---> BDD-cost: 77 c ---[ 77]---> BDD-cost: 77 c ---[ 76]---> BDD-cost: 77 c ---[ 75]---> BDD-cost: 77 c ---[ 74]---> BDD-cost: 77 c ---[ 73]---> BDD-cost: 77 c ---[ 72]---> BDD-cost: 77 c ---[ 71]---> BDD-cost: 77 c ---[ 70]---> BDD-cost: 77 c ---[ 69]---> BDD-cost: 77 c ---[ 68]---> BDD-cost: 77 c ---[ 67]---> BDD-cost: 77 c ---[ 66]---> BDD-cost: 77 c ---[ 65]---> BDD-cost: 77 c ---[ 64]---> BDD-cost: 77 c ---[ 63]---> BDD-cost: 77 c ---[ 62]---> BDD-cost: 77 c ---[ 61]---> BDD-cost: 77 c ---[ 60]---> BDD-cost: 77 c ---[ 59]---> BDD-cost: 77 c ---[ 58]---> BDD-cost: 77 c ---[ 57]---> BDD-cost: 77 c ---[ 56]---> BDD-cost: 77 c ---[ 55]---> BDD-cost: 77 c ---[ 54]---> BDD-cost: 77 c ---[ 53]---> BDD-cost: 77 c ---[ 52]---> BDD-cost: 77 c ---[ 51]---> BDD-cost: 77 c ---[ 50]---> BDD-cost: 77 c ---[ 49]---> BDD-cost: 77 c ---[ 48]---> BDD-cost: 77 c ---[ 47]---> BDD-cost: 77 c ---[ 46]---> BDD-cost: 77 c ---[ 45]---> BDD-cost: 77 c ---[ 44]---> BDD-cost: 77 c ---[ 43]---> BDD-cost: 77 c ---[ 42]---> BDD-cost: 77 c ---[ 41]---> BDD-cost: 77 c ---[ 40]---> BDD-cost: 77 c ---[ 39]---> BDD-cost: 37 c ---[ 38]---> BDD-cost: 37 c ---[ 37]---> BDD-cost: 37 c ---[ 36]---> BDD-cost: 37 c ---[ 35]---> BDD-cost: 37 c ---[ 34]---> BDD-cost: 37 c ---[ 33]---> BDD-cost: 37 c ---[ 32]---> BDD-cost: 37 c ---[ 31]---> BDD-cost: 37 c ---[ 30]---> BDD-cost: 37 c ---[ 29]---> BDD-cost: 37 c ---[ 28]---> BDD-cost: 37 c ---[ 27]---> BDD-cost: 37 c ---[ 26]---> BDD-cost: 37 c ---[ 25]---> BDD-cost: 37 c ---[ 24]---> BDD-cost: 37 c ---[ 23]---> BDD-cost: 37 c ---[ 22]---> BDD-cost: 37 c ---[ 21]---> BDD-cost: 37 c ---[ 20]---> BDD-cost: 37 c ---[ 19]---> BDD-cost: 37 c ---[ 18]---> BDD-cost: 37 c ---[ 17]---> BDD-cost: 37 c ---[ 16]---> BDD-cost: 37 c ---[ 15]---> BDD-cost: 37 c ---[ 14]---> BDD-cost: 37 c ---[ 13]---> BDD-cost: 37 c ---[ 12]---> BDD-cost: 37 c ---[ 11]---> BDD-cost: 37 c ---[ 10]---> BDD-cost: 37 c ---[ 9]---> BDD-cost: 37 c ---[ 8]---> BDD-cost: 37 c ---[ 7]---> BDD-cost: 37 c ---[ 6]---> BDD-cost: 37 c ---[ 5]---> BDD-cost: 37 c ---[ 4]---> BDD-cost: 37 c ---[ 3]---> BDD-cost: 37 c ---[ 2]---> BDD-cost: 37 c ---[ 1]---> BDD-cost: 37 c ---[ 0]---> BDD-cost: 37 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12920 64560 | 4306 0 0 nan | 0.000 % | c | 100 | 12920 64560 | 4736 100 26004 260.0 | 1.149 % | c | 252 | 12920 64560 | 5210 252 37714 149.7 | 1.150 % | c | 477 | 12920 64560 | 5731 477 76875 161.2 | 1.149 % | c | 814 | 12920 64560 | 6304 814 161811 198.8 | 1.149 % | c | 1321 | 12920 64560 | 6934 1321 261531 198.0 | 1.149 % | c | 2084 | 12920 64560 | 7628 2084 359745 172.6 | 1.149 % | c | 3223 | 12920 64560 | 8391 3223 791517 245.6 | 1.149 % | c | 4932 | 12920 64560 | 9230 4932 1197916 242.9 | 1.149 % | c | 7496 | 12920 64560 | 10153 7496 2266760 302.4 | 1.150 % | c | 11341 | 12920 64560 | 11168 11341 3377694 297.8 | 1.149 % | c | 17108 | 12920 64560 | 12285 11438 4096533 358.2 | 1.149 % | c | 25758 | 12920 64560 | 13514 12002 3744055 312.0 | 1.149 % | c | 38732 | 12920 64560 | 14865 15473 2381199 153.9 | 1.149 % | c | 58193 | 12920 64560 | 16352 17728 7855736 443.1 | 1.149 % | c | 87385 | 12920 64560 | 17987 17936 6971394 388.7 | 1.149 % | c | 131175 | 12920 64560 | 19785 15044 2526709 168.0 | 1.149 % | c | 196861 | 12920 64560 | 21764 20319 9340279 459.7 | 1.149 % | c | 295389 | 12920 64560 | 23941 18363 2895214 157.7 | 1.149 % |
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/25130/stat): 25130 (minisat+_script) R 25129 25130 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783101960 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/25130/statm): 174 3 169 147 0 27 0 [pid=25130] 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=25131 New process pid=25132 New process pid=25133 execve syscall for /bin/sed executable One traced child (pid=25132) 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=25133) exited with status: 0 One traced child (pid=25131) exited with status: 0 New process pid=25134 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-fpga40_40_sat_pb.cnf.cr.opb [startup+10.0046 s] Raw data (loadavg): 0.94 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 2798 0 2 0 948 12 0 0 25 0 1 0 1783101965 11763712 2786 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 2872 2786 145 145 0 2727 0 [pid=25134] vsize: 11488 Current children cumulated CPU time (s) 9.6 Current children cumulated vsize (Kb) 13612 [startup+20.0051 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 4298 0 2 0 1923 23 0 0 25 0 1 0 1783101965 17928192 4286 4294967295 134512640 135094434 3221224432 3221223024 134556908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 4377 4286 145 145 0 4232 0 [pid=25134] vsize: 17508 Current children cumulated CPU time (s) 19.46 Current children cumulated vsize (Kb) 19632 [startup+30.0057 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 4746 0 2 0 2916 26 0 0 25 0 1 0 1783101965 19763200 4734 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 4825 4734 145 145 0 4680 0 [pid=25134] vsize: 19300 Current children cumulated CPU time (s) 29.42 Current children cumulated vsize (Kb) 21424 [startup+40.0063 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6286 0 2 0 3897 34 0 0 25 0 1 0 1783101965 26062848 6274 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 6363 6274 145 145 0 6218 0 [pid=25134] vsize: 25452 Current children cumulated CPU time (s) 39.31 Current children cumulated vsize (Kb) 27576 [startup+50.0078 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 4891 35 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0 [pid=25134] vsize: 26636 Current children cumulated CPU time (s) 49.26 Current children cumulated vsize (Kb) 28760 [startup+60.0084 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 5891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0 [pid=25134] vsize: 26636 Current children cumulated CPU time (s) 59.27 Current children cumulated vsize (Kb) 28760 [startup+70.0089 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 6891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0 [pid=25134] vsize: 26636 Current children cumulated CPU time (s) 69.27 Current children cumulated vsize (Kb) 28760 [startup+80.0095 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 7891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0 [pid=25134] vsize: 26636 Current children cumulated CPU time (s) 79.27 Current children cumulated vsize (Kb) 28760 [startup+90.009 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6584 0 2 0 8891 36 0 0 25 0 1 0 1783101965 27275264 6572 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 6659 6572 145 145 0 6514 0 [pid=25134] vsize: 26636 Current children cumulated CPU time (s) 89.27 Current children cumulated vsize (Kb) 28760 [startup+100.01 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 6925 0 2 0 9886 39 0 0 25 0 1 0 1783101965 28700672 6913 4294967295 134512640 135094434 3221224432 3221223024 134557334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 7007 6913 145 145 0 6862 0 [pid=25134] vsize: 28028 Current children cumulated CPU time (s) 99.25 Current children cumulated vsize (Kb) 30152 [startup+110.01 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7419 0 2 0 10878 42 0 0 25 0 1 0 1783101965 30748672 7407 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 7507 7407 145 145 0 7362 0 [pid=25134] vsize: 30028 Current children cumulated CPU time (s) 109.2 Current children cumulated vsize (Kb) 32152 [startup+120.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7468 0 2 0 11878 42 0 0 25 0 1 0 1783101965 30953472 7456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 7557 7456 145 145 0 7412 0 [pid=25134] vsize: 30228 Current children cumulated CPU time (s) 119.2 Current children cumulated vsize (Kb) 32352 [startup+130.011 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7487 0 2 0 12878 42 0 0 25 0 1 0 1783101965 31019008 7475 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 7573 7475 145 145 0 7428 0 [pid=25134] vsize: 30292 Current children cumulated CPU time (s) 129.2 Current children cumulated vsize (Kb) 32416 [startup+140.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 7547 0 2 0 13877 42 0 0 25 0 1 0 1783101965 31322112 7535 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 7647 7535 145 145 0 7502 0 [pid=25134] vsize: 30588 Current children cumulated CPU time (s) 139.19 Current children cumulated vsize (Kb) 32712 [startup+150.012 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 8084 0 2 0 14869 47 0 0 25 0 1 0 1783101965 33521664 8072 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 8184 8072 145 145 0 8039 0 [pid=25134] vsize: 32736 Current children cumulated CPU time (s) 149.16 Current children cumulated vsize (Kb) 34860 [startup+160.013 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 8805 0 2 0 15859 51 0 0 25 0 1 0 1783101965 36511744 8793 4294967295 134512640 135094434 3221224432 3221223024 134557020 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 8914 8793 145 145 0 8769 0 [pid=25134] vsize: 35656 Current children cumulated CPU time (s) 159.1 Current children cumulated vsize (Kb) 37780 [startup+170.014 s] Raw data (loadavg): 1.07 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9532 0 2 0 16847 55 0 0 25 0 1 0 1783101965 39505920 9520 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9645 9520 145 145 0 9500 0 [pid=25134] vsize: 38580 Current children cumulated CPU time (s) 169.02 Current children cumulated vsize (Kb) 40704 [startup+180.014 s] Raw data (loadavg): 1.06 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 17846 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 179.02 Current children cumulated vsize (Kb) 40856 [startup+190.015 s] Raw data (loadavg): 1.05 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 18847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 189.03 Current children cumulated vsize (Kb) 40856 [startup+200.016 s] Raw data (loadavg): 1.04 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 19847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 199.03 Current children cumulated vsize (Kb) 40856 [startup+210.017 s] Raw data (loadavg): 1.03 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 20847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 209.03 Current children cumulated vsize (Kb) 40856 [startup+220.017 s] Raw data (loadavg): 1.03 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 21847 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 219.03 Current children cumulated vsize (Kb) 40856 [startup+230.018 s] Raw data (loadavg): 1.02 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 22848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 229.04 Current children cumulated vsize (Kb) 40856 [startup+240.017 s] Raw data (loadavg): 1.02 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 23848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 239.04 Current children cumulated vsize (Kb) 40856 [startup+250.018 s] Raw data (loadavg): 1.02 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 24848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 249.04 Current children cumulated vsize (Kb) 40856 [startup+260.02 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9570 0 2 0 25848 56 0 0 25 0 1 0 1783101965 39661568 9558 4294967295 134512640 135094434 3221224432 3221223024 134557251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9683 9558 145 145 0 9538 0 [pid=25134] vsize: 38732 Current children cumulated CPU time (s) 259.04 Current children cumulated vsize (Kb) 40856 [startup+270.019 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9855 0 2 0 26844 57 0 0 25 0 1 0 1783101965 40853504 9843 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 9974 9843 145 145 0 9829 0 [pid=25134] vsize: 39896 Current children cumulated CPU time (s) 269.01 Current children cumulated vsize (Kb) 42020 [startup+280.02 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9882 0 2 0 27844 58 0 0 25 0 1 0 1783101965 41037824 9870 4294967295 134512640 135094434 3221224432 3221223104 134555335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 10019 9870 145 145 0 9874 0 [pid=25134] vsize: 40076 Current children cumulated CPU time (s) 279.02 Current children cumulated vsize (Kb) 42200 [startup+290.02 s] Raw data (loadavg): 1.01 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9905 0 2 0 28844 58 0 0 25 0 1 0 1783101965 41168896 9893 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 10051 9893 145 145 0 9906 0 [pid=25134] vsize: 40204 Current children cumulated CPU time (s) 289.02 Current children cumulated vsize (Kb) 42328 [startup+300.021 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9957 0 2 0 29844 58 0 0 25 0 1 0 1783101965 41496576 9945 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 10131 9945 145 145 0 9986 0 [pid=25134] vsize: 40524 Current children cumulated CPU time (s) 299.02 Current children cumulated vsize (Kb) 42648 [startup+310.021 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 9960 0 2 0 30844 58 0 0 25 0 1 0 1783101965 41496576 9948 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 10131 9948 145 145 0 9986 0 [pid=25134] vsize: 40524 Current children cumulated CPU time (s) 309.02 Current children cumulated vsize (Kb) 42648 [startup+320.022 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 31829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 318.94 Current children cumulated vsize (Kb) 46940 [startup+330.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 32829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 328.94 Current children cumulated vsize (Kb) 46940 [startup+340.022 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 33829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 338.94 Current children cumulated vsize (Kb) 46940 [startup+350.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 34829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 348.94 Current children cumulated vsize (Kb) 46940 [startup+360.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 35829 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 358.94 Current children cumulated vsize (Kb) 46940 [startup+370.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 36830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 368.95 Current children cumulated vsize (Kb) 46940 [startup+380.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 37830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 378.95 Current children cumulated vsize (Kb) 46940 [startup+390.023 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 38830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 388.95 Current children cumulated vsize (Kb) 46940 [startup+400.024 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 39830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 398.95 Current children cumulated vsize (Kb) 46940 [startup+410.024 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 40830 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134556982 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 408.95 Current children cumulated vsize (Kb) 46940 [startup+420.024 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 41831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 418.96 Current children cumulated vsize (Kb) 46940 [startup+430.024 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 42831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223024 134557319 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 428.96 Current children cumulated vsize (Kb) 46940 [startup+440.025 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 43831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 438.96 Current children cumulated vsize (Kb) 46940 [startup+450.025 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 44831 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 448.96 Current children cumulated vsize (Kb) 46940 [startup+460.026 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 11033 0 2 0 45832 65 0 0 25 0 1 0 1783101965 45891584 11021 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 11204 11021 145 145 0 11059 0 [pid=25134] vsize: 44816 Current children cumulated CPU time (s) 458.97 Current children cumulated vsize (Kb) 46940 [startup+470.025 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 12399 0 2 0 46810 75 0 0 25 0 1 0 1783101965 51486720 12387 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 12570 12387 145 145 0 12425 0 [pid=25134] vsize: 50280 Current children cumulated CPU time (s) 468.85 Current children cumulated vsize (Kb) 52404 [startup+480.026 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13669 0 2 0 47789 85 0 0 25 0 1 0 1783101965 56692736 13657 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 13841 13657 145 145 0 13696 0 [pid=25134] vsize: 55364 Current children cumulated CPU time (s) 478.74 Current children cumulated vsize (Kb) 57488 [startup+490.027 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 48788 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0 [pid=25134] vsize: 55544 Current children cumulated CPU time (s) 488.73 Current children cumulated vsize (Kb) 57668 [startup+500.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 49789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0 [pid=25134] vsize: 55544 Current children cumulated CPU time (s) 498.74 Current children cumulated vsize (Kb) 57668 [startup+510.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 50789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0 [pid=25134] vsize: 55544 Current children cumulated CPU time (s) 508.74 Current children cumulated vsize (Kb) 57668 [startup+520.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13714 0 2 0 51789 85 0 0 25 0 1 0 1783101965 56877056 13702 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 13886 13702 145 145 0 13741 0 [pid=25134] vsize: 55544 Current children cumulated CPU time (s) 518.74 Current children cumulated vsize (Kb) 57668 [startup+530.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 13986 0 2 0 52786 86 0 0 25 0 1 0 1783101965 57991168 13974 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14158 13974 145 145 0 14013 0 [pid=25134] vsize: 56632 Current children cumulated CPU time (s) 528.72 Current children cumulated vsize (Kb) 58756 [startup+540.028 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14196 0 2 0 53783 88 0 0 25 0 1 0 1783101965 58855424 14184 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14184 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 538.71 Current children cumulated vsize (Kb) 59600 [startup+550.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 54783 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 548.71 Current children cumulated vsize (Kb) 59600 [startup+560.029 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 55784 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 558.72 Current children cumulated vsize (Kb) 59600 [startup+570.03 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14197 0 2 0 56784 88 0 0 25 0 1 0 1783101965 58855424 14185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14185 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 568.72 Current children cumulated vsize (Kb) 59600 [startup+580.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 57784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 578.72 Current children cumulated vsize (Kb) 59600 [startup+590.031 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 58784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 588.72 Current children cumulated vsize (Kb) 59600 [startup+600.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 59784 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 598.72 Current children cumulated vsize (Kb) 59600 [startup+610.032 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 60785 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223076 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 608.73 Current children cumulated vsize (Kb) 59600 [startup+620.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14198 0 2 0 61785 88 0 0 25 0 1 0 1783101965 58855424 14186 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14369 14186 145 145 0 14224 0 [pid=25134] vsize: 57476 Current children cumulated CPU time (s) 618.73 Current children cumulated vsize (Kb) 59600 [startup+630.033 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14329 0 2 0 62783 88 0 0 25 0 1 0 1783101965 59392000 14317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14500 14317 145 145 0 14355 0 [pid=25134] vsize: 58000 Current children cumulated CPU time (s) 628.71 Current children cumulated vsize (Kb) 60124 [startup+640.034 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 63783 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0 [pid=25134] vsize: 58164 Current children cumulated CPU time (s) 638.72 Current children cumulated vsize (Kb) 60288 [startup+650.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 64783 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0 [pid=25134] vsize: 58164 Current children cumulated CPU time (s) 648.72 Current children cumulated vsize (Kb) 60288 [startup+660.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 65784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0 [pid=25134] vsize: 58164 Current children cumulated CPU time (s) 658.73 Current children cumulated vsize (Kb) 60288 [startup+670.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 66784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0 [pid=25134] vsize: 58164 Current children cumulated CPU time (s) 668.73 Current children cumulated vsize (Kb) 60288 [startup+680.035 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14370 0 2 0 67784 89 0 0 25 0 1 0 1783101965 59559936 14358 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/25134/statm): 14541 14358 145 145 0 14396 0 [pid=25134] vsize: 58164 Current children cumulated CPU time (s) 678.73 Current children cumulated vsize (Kb) 60288 [startup+690.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 68782 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 688.72 Current children cumulated vsize (Kb) 60768 [startup+700.036 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 69782 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 698.72 Current children cumulated vsize (Kb) 60768 [startup+710.037 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 70783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 708.73 Current children cumulated vsize (Kb) 60768 [startup+720.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 71783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 718.73 Current children cumulated vsize (Kb) 60768 [startup+730.038 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 72783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 728.73 Current children cumulated vsize (Kb) 60768 [startup+740.039 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 73783 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 738.73 Current children cumulated vsize (Kb) 60768 [startup+750.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 74784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 748.74 Current children cumulated vsize (Kb) 60768 [startup+760.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 75784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134557111 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 758.74 Current children cumulated vsize (Kb) 60768 [startup+770.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 76784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223080 134556677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 768.74 Current children cumulated vsize (Kb) 60768 [startup+780.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 77784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 778.74 Current children cumulated vsize (Kb) 60768 [startup+790.04 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 78784 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 788.74 Current children cumulated vsize (Kb) 60768 [startup+800.041 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 79785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 798.75 Current children cumulated vsize (Kb) 60768 [startup+810.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 80785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 808.75 Current children cumulated vsize (Kb) 60768 [startup+820.042 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 81785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 818.75 Current children cumulated vsize (Kb) 60768 [startup+830.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 82785 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 828.75 Current children cumulated vsize (Kb) 60768 [startup+840.043 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 83786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 838.76 Current children cumulated vsize (Kb) 60768 [startup+850.045 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 84786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 848.76 Current children cumulated vsize (Kb) 60768 [startup+860.045 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 85786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 858.76 Current children cumulated vsize (Kb) 60768 [startup+870.046 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 86786 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 868.76 Current children cumulated vsize (Kb) 60768 [startup+880.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 87787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 878.77 Current children cumulated vsize (Kb) 60768 [startup+890.047 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 88787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 888.77 Current children cumulated vsize (Kb) 60768 [startup+900.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 89787 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 898.77 Current children cumulated vsize (Kb) 60768 [startup+910.049 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 90788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 908.78 Current children cumulated vsize (Kb) 60768 [startup+920.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 91788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 918.78 Current children cumulated vsize (Kb) 60768 [startup+930.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 92788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 928.78 Current children cumulated vsize (Kb) 60768 [startup+940.051 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 93788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 938.78 Current children cumulated vsize (Kb) 60768 [startup+950.052 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 94788 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 948.78 Current children cumulated vsize (Kb) 60768 [startup+960.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 95789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 958.79 Current children cumulated vsize (Kb) 60768 [startup+970.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 96789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 968.79 Current children cumulated vsize (Kb) 60768 [startup+980.053 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 97789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 978.79 Current children cumulated vsize (Kb) 60768 [startup+990.054 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 14490 0 2 0 98789 90 0 0 25 0 1 0 1783101965 60051456 14478 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 14661 14478 145 145 0 14516 0 [pid=25134] vsize: 58644 Current children cumulated CPU time (s) 988.79 Current children cumulated vsize (Kb) 60768 [startup+1000.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 15039 0 2 0 99781 94 0 0 25 0 1 0 1783101965 62304256 15027 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 15211 15027 145 145 0 15066 0 [pid=25134] vsize: 60844 Current children cumulated CPU time (s) 998.75 Current children cumulated vsize (Kb) 62968 [startup+1010.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 15845 0 2 0 100766 101 0 0 25 0 1 0 1783101965 65617920 15833 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 16020 15833 145 145 0 15875 0 [pid=25134] vsize: 64080 Current children cumulated CPU time (s) 1008.67 Current children cumulated vsize (Kb) 66204 [startup+1020.05 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 16533 0 2 0 101756 105 0 0 25 0 1 0 1783101965 68435968 16521 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 16708 16521 145 145 0 16563 0 [pid=25134] vsize: 66832 Current children cumulated CPU time (s) 1018.61 Current children cumulated vsize (Kb) 68956 [startup+1030.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17016 0 2 0 102748 108 0 0 25 0 1 0 1783101965 70447104 17004 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17199 17004 145 145 0 17054 0 [pid=25134] vsize: 68796 Current children cumulated CPU time (s) 1028.56 Current children cumulated vsize (Kb) 70920 [startup+1040.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17273 0 2 0 103744 110 0 0 25 0 1 0 1783101965 71491584 17261 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17261 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1038.54 Current children cumulated vsize (Kb) 71940 [startup+1050.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17274 0 2 0 104744 110 0 0 25 0 1 0 1783101965 71491584 17262 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17262 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1048.54 Current children cumulated vsize (Kb) 71940 [startup+1060.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 105745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1058.55 Current children cumulated vsize (Kb) 71940 [startup+1070.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 106745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1068.55 Current children cumulated vsize (Kb) 71940 [startup+1080.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 107745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1078.55 Current children cumulated vsize (Kb) 71940 [startup+1090.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 108745 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1088.55 Current children cumulated vsize (Kb) 71940 [startup+1100.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 109746 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1098.56 Current children cumulated vsize (Kb) 71940 [startup+1110.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17275 0 2 0 110746 110 0 0 25 0 1 0 1783101965 71491584 17263 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17263 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1108.56 Current children cumulated vsize (Kb) 71940 [startup+1120.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 111746 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1118.56 Current children cumulated vsize (Kb) 71940 [startup+1130.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 112746 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1128.56 Current children cumulated vsize (Kb) 71940 [startup+1140.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 113747 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1138.57 Current children cumulated vsize (Kb) 71940 [startup+1150.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17278 0 2 0 114747 110 0 0 25 0 1 0 1783101965 71491584 17266 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17454 17266 145 145 0 17309 0 [pid=25134] vsize: 69816 Current children cumulated CPU time (s) 1148.57 Current children cumulated vsize (Kb) 71940 [startup+1160.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 17641 0 2 0 115741 113 0 0 25 0 1 0 1783101965 72990720 17629 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 17820 17629 145 145 0 17675 0 [pid=25134] vsize: 71280 Current children cumulated CPU time (s) 1158.54 Current children cumulated vsize (Kb) 73404 [startup+1170.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 18098 0 2 0 116733 116 0 0 25 0 1 0 1783101965 74866688 18086 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 18278 18086 145 145 0 18133 0 [pid=25134] vsize: 73112 Current children cumulated CPU time (s) 1168.49 Current children cumulated vsize (Kb) 75236 [startup+1180.06 s] Raw data (loadavg): 1.00 1.00 1.00 1/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) T 25130 25130 22582 0 -1 0 18729 0 2 0 117723 121 0 0 25 0 1 0 1783101965 77443072 18717 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/25134/statm): 18907 18717 145 145 0 18762 0 [pid=25134] vsize: 75628 Current children cumulated CPU time (s) 1178.44 Current children cumulated vsize (Kb) 77752 [startup+1190.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 19121 0 2 0 118718 123 0 0 25 0 1 0 1783101965 79077376 19109 4294967295 134512640 135094434 3221224432 3221223024 134556779 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 19306 19109 145 145 0 19161 0 [pid=25134] vsize: 77224 Current children cumulated CPU time (s) 1188.41 Current children cumulated vsize (Kb) 79348 [startup+1200.06 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 19567 0 2 0 119710 127 0 0 25 0 1 0 1783101965 80900096 19555 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 19751 19555 145 145 0 19606 0 [pid=25134] vsize: 79004 Current children cumulated CPU time (s) 1198.37 Current children cumulated vsize (Kb) 81128 [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 20125 0 2 0 120701 130 0 0 25 0 1 0 1783101965 83206144 20113 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 20314 20113 145 145 0 20169 0 [pid=25134] vsize: 81256 Current children cumulated CPU time (s) 1208.31 Current children cumulated vsize (Kb) 83380 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 1.00 1.00 1.00 2/57 25134 Raw data (/proc/25130/stat): 25130 (minisat+_script) S 25129 25130 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1783101960 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/25130/statm): 531 226 485 147 0 384 0 [pid=25130] vsize: 2124 Raw data (/proc/25134/stat): 25134 (minisat+_64-bit) R 25130 25130 22582 0 -1 0 20125 0 2 0 120701 130 0 0 25 0 1 0 1783101965 83206144 20113 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/25134/statm): 20314 20113 145 145 0 20169 0 [pid=25134] vsize: 81256 Current children cumulated CPU time (s) 1208.31 Current children cumulated vsize (Kb) 83380 Sending SIGTERM to -25130 Sleeping 2 seconds One traced child (pid=25130) ended because it received signal 15 (SIGTERM) One traced child (pid=25134) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.11 CPU time (s): 1208.36 CPU user time (s): 1207.01 CPU system time (s): 1.3448 CPU usage (%): 99.8555 Max. virtual memory (cumulated for all children) (Kb): 83380
ERROR: no interpretation found !