Name | submitted/aloul/FPGA_SAT05/normalized-fpga40_38_sat_pb.cnf.cr.opb |
MD5SUM | 69d239b72e8d1a72f9c55329043493e1 |
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 | 14.9957 |
Number of variables | 2280 |
Total number of constraints | 1636 |
Number of constraints which are clauses | 1558 |
Number of constraints which are cardinality constraints (but not clauses) | 78 |
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 wulflinc4 THE 2005-09-18 12:33:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2391 boxname=wulflinc4 idbench=47 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 69d239b72e8d1a72f9c55329043493e1 /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb IDLAUNCH: 2391 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 945544 kB Buffers: 33908 kB Cached: 31364 kB SwapCached: 960 kB Active: 52748 kB Inactive: 15204 kB HighTotal: 131008 kB HighFree: 97188 kB LowTotal: 903652 kB LowFree: 848356 kB SwapTotal: 2097136 kB SwapFree: 2095628 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5692 kB Slab: 15524 kB Committed_AS: 72360 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:54:05 (client local time) WITH STATUS 0 IN 1208.81 SECONDS stats: 2391 7 1208.81 0
c Parsing PB file... c Converting 1636 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 77]---> BDD-cost: 73 c ---[ 76]---> BDD-cost: 73 c ---[ 75]---> BDD-cost: 73 c ---[ 74]---> BDD-cost: 73 c ---[ 73]---> BDD-cost: 73 c ---[ 72]---> BDD-cost: 73 c ---[ 71]---> BDD-cost: 73 c ---[ 70]---> BDD-cost: 73 c ---[ 69]---> BDD-cost: 73 c ---[ 68]---> BDD-cost: 73 c ---[ 67]---> BDD-cost: 73 c ---[ 66]---> BDD-cost: 73 c ---[ 65]---> BDD-cost: 73 c ---[ 64]---> BDD-cost: 73 c ---[ 63]---> BDD-cost: 73 c ---[ 62]---> BDD-cost: 73 c ---[ 61]---> BDD-cost: 73 c ---[ 60]---> BDD-cost: 73 c ---[ 59]---> BDD-cost: 73 c ---[ 58]---> BDD-cost: 73 c ---[ 57]---> BDD-cost: 73 c ---[ 56]---> BDD-cost: 73 c ---[ 55]---> BDD-cost: 73 c ---[ 54]---> BDD-cost: 73 c ---[ 53]---> BDD-cost: 73 c ---[ 52]---> BDD-cost: 73 c ---[ 51]---> BDD-cost: 73 c ---[ 50]---> BDD-cost: 73 c ---[ 49]---> BDD-cost: 73 c ---[ 48]---> BDD-cost: 73 c ---[ 47]---> BDD-cost: 73 c ---[ 46]---> BDD-cost: 73 c ---[ 45]---> BDD-cost: 73 c ---[ 44]---> BDD-cost: 73 c ---[ 43]---> BDD-cost: 73 c ---[ 42]---> BDD-cost: 73 c ---[ 41]---> BDD-cost: 73 c ---[ 40]---> BDD-cost: 73 c ---[ 39]---> BDD-cost: 73 c ---[ 38]---> BDD-cost: 73 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 | 12256 59766 | 4085 0 0 nan | 0.000 % | c | 103 | 12256 59766 | 4493 103 23189 225.1 | 1.181 % | c | 253 | 12256 59766 | 4942 253 33793 133.6 | 1.181 % | c | 480 | 12256 59766 | 5437 480 75308 156.9 | 1.181 % | c | 817 | 12256 59766 | 5980 817 169756 207.8 | 1.181 % | c | 1323 | 12256 59766 | 6578 1323 266622 201.5 | 1.181 % | c | 2082 | 12256 59766 | 7236 2082 346944 166.6 | 1.181 % | c | 3221 | 12256 59766 | 7960 3221 672994 208.9 | 1.181 % | c | 4933 | 12256 59766 | 8756 4933 891745 180.8 | 1.181 % | c | 7495 | 12256 59766 | 9632 7495 1795103 239.5 | 1.181 % | c | 11340 | 12256 59766 | 10595 11340 2331890 205.6 | 1.181 % | c | 17107 | 12256 59766 | 11654 11437 3336088 291.7 | 1.181 % | c | 25760 | 12256 59766 | 12820 12101 3971454 328.2 | 1.181 % | c | 38736 | 12256 59766 | 14102 16761 4472808 266.9 | 1.181 % | c | 58201 | 12256 59766 | 15512 18480 7868227 425.8 | 1.181 % | c | 87394 | 12256 59766 | 17064 17668 2277590 128.9 | 1.181 % | c | 131184 | 12256 59766 | 18770 21073 9678978 459.3 | 1.181 % | c | 196873 | 12256 59766 | 20647 20482 7435518 363.0 | 1.181 % | c | 295403 | 12256 59766 | 22712 24813 4118111 166.0 | 1.181 % |
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/9432/stat): 9432 (minisat+_script) R 9431 9432 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1783047228 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/9432/statm): 174 3 169 147 0 27 0 [pid=9432] 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=9433 New process pid=9434 New process pid=9435 execve syscall for /bin/sed executable One traced child (pid=9434) 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=9435) exited with status: 0 One traced child (pid=9433) exited with status: 0 New process pid=9436 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-fpga40_38_sat_pb.cnf.cr.opb [startup+10.004 s] Raw data (loadavg): 0.82 0.91 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 2710 0 0 0 962 15 0 0 25 0 1 0 1783047233 11395072 2696 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 2782 2696 145 145 0 2637 0 [pid=9436] vsize: 11128 Current children cumulated CPU time (s) 9.78 Current children cumulated vsize (Kb) 13252 [startup+20.0058 s] Raw data (loadavg): 0.85 0.91 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 3212 0 0 0 1955 18 0 0 25 0 1 0 1783047233 13467648 3198 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 3288 3198 145 145 0 3143 0 [pid=9436] vsize: 13152 Current children cumulated CPU time (s) 19.74 Current children cumulated vsize (Kb) 15276 [startup+30.0076 s] Raw data (loadavg): 0.87 0.91 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 4573 0 0 0 2935 26 0 0 25 0 1 0 1783047233 19066880 4559 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 4655 4559 145 145 0 4510 0 [pid=9436] vsize: 18620 Current children cumulated CPU time (s) 29.62 Current children cumulated vsize (Kb) 20744 [startup+40.0074 s] Raw data (loadavg): 0.89 0.91 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5754 0 0 0 3917 35 0 0 25 0 1 0 1783047233 23916544 5740 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 5839 5740 145 145 0 5694 0 [pid=9436] vsize: 23356 Current children cumulated CPU time (s) 39.53 Current children cumulated vsize (Kb) 25480 [startup+50.0092 s] Raw data (loadavg): 0.91 0.92 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5786 0 0 0 4917 35 0 0 25 0 1 0 1783047233 24031232 5772 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 5867 5772 145 145 0 5722 0 [pid=9436] vsize: 23468 Current children cumulated CPU time (s) 49.53 Current children cumulated vsize (Kb) 25592 [startup+60.0101 s] Raw data (loadavg): 0.92 0.92 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 5787 0 0 0 5917 35 0 0 25 0 1 0 1783047233 24031232 5773 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 5867 5773 145 145 0 5722 0 [pid=9436] vsize: 23468 Current children cumulated CPU time (s) 59.53 Current children cumulated vsize (Kb) 25592 [startup+70.0119 s] Raw data (loadavg): 0.93 0.92 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 6905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0 [pid=9436] vsize: 26620 Current children cumulated CPU time (s) 69.45 Current children cumulated vsize (Kb) 28744 [startup+80.0127 s] Raw data (loadavg): 0.94 0.92 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 7905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0 [pid=9436] vsize: 26620 Current children cumulated CPU time (s) 79.45 Current children cumulated vsize (Kb) 28744 [startup+90.0135 s] Raw data (loadavg): 0.95 0.92 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 8905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0 [pid=9436] vsize: 26620 Current children cumulated CPU time (s) 89.45 Current children cumulated vsize (Kb) 28744 [startup+100.014 s] Raw data (loadavg): 0.96 0.93 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 6560 0 0 0 9905 39 0 0 25 0 1 0 1783047233 27258880 6546 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 6655 6546 145 145 0 6510 0 [pid=9436] vsize: 26620 Current children cumulated CPU time (s) 99.45 Current children cumulated vsize (Kb) 28744 [startup+110.015 s] Raw data (loadavg): 0.96 0.93 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 10894 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0 [pid=9436] vsize: 29156 Current children cumulated CPU time (s) 109.39 Current children cumulated vsize (Kb) 31280 [startup+120.017 s] Raw data (loadavg): 0.97 0.93 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 11895 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0 [pid=9436] vsize: 29156 Current children cumulated CPU time (s) 119.4 Current children cumulated vsize (Kb) 31280 [startup+130.018 s] Raw data (loadavg): 0.97 0.93 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7194 0 0 0 12895 44 0 0 25 0 1 0 1783047233 29855744 7180 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 7289 7180 145 145 0 7144 0 [pid=9436] vsize: 29156 Current children cumulated CPU time (s) 129.4 Current children cumulated vsize (Kb) 31280 [startup+140.019 s] Raw data (loadavg): 0.98 0.93 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7195 0 0 0 13894 44 0 0 25 0 1 0 1783047233 29855744 7181 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 7289 7181 145 145 0 7144 0 [pid=9436] vsize: 29156 Current children cumulated CPU time (s) 139.39 Current children cumulated vsize (Kb) 31280 [startup+150.02 s] Raw data (loadavg): 0.98 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7363 0 0 0 14891 46 0 0 25 0 1 0 1783047233 30552064 7349 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 7459 7349 145 145 0 7314 0 [pid=9436] vsize: 29836 Current children cumulated CPU time (s) 149.38 Current children cumulated vsize (Kb) 31960 [startup+160.02 s] Raw data (loadavg): 0.98 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 7941 0 0 0 15883 49 0 0 25 0 1 0 1783047233 32956416 7927 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 8046 7927 145 145 0 7901 0 [pid=9436] vsize: 32184 Current children cumulated CPU time (s) 159.33 Current children cumulated vsize (Kb) 34308 [startup+170.022 s] Raw data (loadavg): 0.98 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 8535 0 0 0 16874 52 0 0 25 0 1 0 1783047233 35405824 8521 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 8644 8521 145 145 0 8499 0 [pid=9436] vsize: 34576 Current children cumulated CPU time (s) 169.27 Current children cumulated vsize (Kb) 36700 [startup+180.023 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9138 0 0 0 17865 56 0 0 25 0 1 0 1783047233 37900288 9124 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9253 9124 145 145 0 9108 0 [pid=9436] vsize: 37012 Current children cumulated CPU time (s) 179.22 Current children cumulated vsize (Kb) 39136 [startup+190.024 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9606 0 0 0 18857 59 0 0 25 0 1 0 1783047233 39825408 9592 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9592 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 189.17 Current children cumulated vsize (Kb) 41016 [startup+200.026 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 19857 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 199.17 Current children cumulated vsize (Kb) 41016 [startup+210.026 s] Raw data (loadavg): 0.99 0.94 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 20857 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 209.17 Current children cumulated vsize (Kb) 41016 [startup+220.027 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 21858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 219.18 Current children cumulated vsize (Kb) 41016 [startup+230.028 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 22858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 229.18 Current children cumulated vsize (Kb) 41016 [startup+240.029 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 23858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 239.18 Current children cumulated vsize (Kb) 41016 [startup+250.03 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 24858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 249.18 Current children cumulated vsize (Kb) 41016 [startup+260.031 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 25858 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 259.18 Current children cumulated vsize (Kb) 41016 [startup+270.033 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 26859 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 269.19 Current children cumulated vsize (Kb) 41016 [startup+280.033 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9608 0 0 0 27859 59 0 0 25 0 1 0 1783047233 39825408 9594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9594 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 279.19 Current children cumulated vsize (Kb) 41016 [startup+290.034 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 28859 59 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 289.19 Current children cumulated vsize (Kb) 41016 [startup+300.036 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 29859 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 299.2 Current children cumulated vsize (Kb) 41016 [startup+310.037 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 30860 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 309.21 Current children cumulated vsize (Kb) 41016 [startup+320.039 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9609 0 0 0 31860 60 0 0 25 0 1 0 1783047233 39825408 9595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9723 9595 145 145 0 9578 0 [pid=9436] vsize: 38892 Current children cumulated CPU time (s) 319.21 Current children cumulated vsize (Kb) 41016 [startup+330.04 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 9705 0 0 0 32858 62 0 0 25 0 1 0 1783047233 40230912 9691 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 9822 9691 145 145 0 9677 0 [pid=9436] vsize: 39288 Current children cumulated CPU time (s) 329.21 Current children cumulated vsize (Kb) 41412 [startup+340.041 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 10074 0 0 0 33852 63 0 0 25 0 1 0 1783047233 41787392 10060 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 10202 10060 145 145 0 10057 0 [pid=9436] vsize: 40808 Current children cumulated CPU time (s) 339.16 Current children cumulated vsize (Kb) 42932 [startup+350.042 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 10535 0 0 0 34846 66 0 0 25 0 1 0 1783047233 43663360 10521 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 10660 10521 145 145 0 10515 0 [pid=9436] vsize: 42640 Current children cumulated CPU time (s) 349.13 Current children cumulated vsize (Kb) 44764 [startup+360.043 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 11009 0 0 0 35839 70 0 0 25 0 1 0 1783047233 45666304 10995 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 11149 10995 145 145 0 11004 0 [pid=9436] vsize: 44596 Current children cumulated CPU time (s) 359.1 Current children cumulated vsize (Kb) 46720 [startup+370.044 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 11601 0 0 0 36829 74 0 0 25 0 1 0 1783047233 48082944 11587 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 11739 11587 145 145 0 11594 0 [pid=9436] vsize: 46956 Current children cumulated CPU time (s) 369.04 Current children cumulated vsize (Kb) 49080 [startup+380.045 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12011 0 0 0 37823 77 0 0 25 0 1 0 1783047233 49831936 11997 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12166 11997 145 145 0 12021 0 [pid=9436] vsize: 48664 Current children cumulated CPU time (s) 379.01 Current children cumulated vsize (Kb) 50788 [startup+390.046 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 38819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0 [pid=9436] vsize: 49532 Current children cumulated CPU time (s) 388.99 Current children cumulated vsize (Kb) 51656 [startup+400.047 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 39819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0 [pid=9436] vsize: 49532 Current children cumulated CPU time (s) 398.99 Current children cumulated vsize (Kb) 51656 [startup+410.047 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 40819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221222960 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0 [pid=9436] vsize: 49532 Current children cumulated CPU time (s) 408.99 Current children cumulated vsize (Kb) 51656 [startup+420.049 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12228 0 0 0 41819 79 0 0 25 0 1 0 1783047233 50720768 12214 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12383 12214 145 145 0 12238 0 [pid=9436] vsize: 49532 Current children cumulated CPU time (s) 418.99 Current children cumulated vsize (Kb) 51656 [startup+430.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 42815 81 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0 [pid=9436] vsize: 50984 Current children cumulated CPU time (s) 428.97 Current children cumulated vsize (Kb) 53108 [startup+440.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 43815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0 [pid=9436] vsize: 50984 Current children cumulated CPU time (s) 438.98 Current children cumulated vsize (Kb) 53108 [startup+450.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 44815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0 [pid=9436] vsize: 50984 Current children cumulated CPU time (s) 448.98 Current children cumulated vsize (Kb) 53108 [startup+460.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 45815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0 [pid=9436] vsize: 50984 Current children cumulated CPU time (s) 458.98 Current children cumulated vsize (Kb) 53108 [startup+470.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12591 0 0 0 46815 82 0 0 25 0 1 0 1783047233 52207616 12577 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12746 12577 145 145 0 12601 0 [pid=9436] vsize: 50984 Current children cumulated CPU time (s) 468.98 Current children cumulated vsize (Kb) 53108 [startup+480.054 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 47815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 478.98 Current children cumulated vsize (Kb) 53176 [startup+490.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 48815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221223024 134556984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 488.98 Current children cumulated vsize (Kb) 53176 [startup+500.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12608 0 0 0 49815 82 0 0 25 0 1 0 1783047233 52277248 12594 4294967295 134512640 135094434 3221224432 3221222992 134550337 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12594 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 498.98 Current children cumulated vsize (Kb) 53176 [startup+510.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 50815 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 508.99 Current children cumulated vsize (Kb) 53176 [startup+520.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 51815 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 518.99 Current children cumulated vsize (Kb) 53176 [startup+530.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 52816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 529 Current children cumulated vsize (Kb) 53176 [startup+540.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 53816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 539 Current children cumulated vsize (Kb) 53176 [startup+550.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 54816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 549 Current children cumulated vsize (Kb) 53176 [startup+560.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 55816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 559 Current children cumulated vsize (Kb) 53176 [startup+570.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 56816 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 569 Current children cumulated vsize (Kb) 53176 [startup+580.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 57817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 579.01 Current children cumulated vsize (Kb) 53176 [startup+590.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 58817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 589.01 Current children cumulated vsize (Kb) 53176 [startup+600.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 59817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 599.01 Current children cumulated vsize (Kb) 53176 [startup+610.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 60817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 609.01 Current children cumulated vsize (Kb) 53176 [startup+620.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 61817 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 619.01 Current children cumulated vsize (Kb) 53176 [startup+630.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 62818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 629.02 Current children cumulated vsize (Kb) 53176 [startup+640.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 63818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 639.02 Current children cumulated vsize (Kb) 53176 [startup+650.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 64818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 649.02 Current children cumulated vsize (Kb) 53176 [startup+660.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 65818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 659.02 Current children cumulated vsize (Kb) 53176 [startup+670.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 66818 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 669.02 Current children cumulated vsize (Kb) 53176 [startup+680.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 67819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221222944 134783385 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 679.03 Current children cumulated vsize (Kb) 53176 [startup+690.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 68819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 689.03 Current children cumulated vsize (Kb) 53176 [startup+700.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 69819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 699.03 Current children cumulated vsize (Kb) 53176 [startup+710.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 70819 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 709.03 Current children cumulated vsize (Kb) 53176 [startup+720.079 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 71820 83 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 719.04 Current children cumulated vsize (Kb) 53176 [startup+730.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 72820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223104 134555758 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 729.05 Current children cumulated vsize (Kb) 53176 [startup+740.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 73820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 739.05 Current children cumulated vsize (Kb) 53176 [startup+750.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 74820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 749.05 Current children cumulated vsize (Kb) 53176 [startup+760.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 75820 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 759.05 Current children cumulated vsize (Kb) 53176 [startup+770.083 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 76821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 769.06 Current children cumulated vsize (Kb) 53176 [startup+780.084 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 77821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 779.06 Current children cumulated vsize (Kb) 53176 [startup+790.085 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 78821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 789.06 Current children cumulated vsize (Kb) 53176 [startup+800.086 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12609 0 0 0 79821 84 0 0 25 0 1 0 1783047233 52277248 12595 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 12763 12595 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 799.06 Current children cumulated vsize (Kb) 53176 [startup+810.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 80820 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 809.05 Current children cumulated vsize (Kb) 53176 [startup+820.088 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 81820 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 819.05 Current children cumulated vsize (Kb) 53176 [startup+830.088 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12611 0 0 0 82821 84 0 0 25 0 1 0 1783047233 52277248 12597 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12597 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 829.06 Current children cumulated vsize (Kb) 53176 [startup+840.089 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 83821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 839.06 Current children cumulated vsize (Kb) 53176 [startup+850.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 84821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 849.06 Current children cumulated vsize (Kb) 53176 [startup+860.091 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 85821 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 859.06 Current children cumulated vsize (Kb) 53176 [startup+870.093 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 86822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 869.07 Current children cumulated vsize (Kb) 53176 [startup+880.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 87822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 879.07 Current children cumulated vsize (Kb) 53176 [startup+890.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 88822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 889.07 Current children cumulated vsize (Kb) 53176 [startup+900.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 89822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 899.07 Current children cumulated vsize (Kb) 53176 [startup+910.095 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 90822 84 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558284 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 909.07 Current children cumulated vsize (Kb) 53176 [startup+920.096 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 91822 85 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 919.08 Current children cumulated vsize (Kb) 53176 [startup+930.097 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 92822 85 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 929.08 Current children cumulated vsize (Kb) 53176 [startup+940.098 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 93821 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 939.08 Current children cumulated vsize (Kb) 53176 [startup+950.099 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 94821 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 949.08 Current children cumulated vsize (Kb) 53176 [startup+960.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 95822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 959.09 Current children cumulated vsize (Kb) 53176 [startup+970.101 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 96822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221221900 134563367 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 969.09 Current children cumulated vsize (Kb) 53176 [startup+980.101 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 97822 86 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 979.09 Current children cumulated vsize (Kb) 53176 [startup+990.102 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 98822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 989.1 Current children cumulated vsize (Kb) 53176 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 99822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134557108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 999.1 Current children cumulated vsize (Kb) 53176 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 100822 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1009.1 Current children cumulated vsize (Kb) 53176 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 101823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1019.11 Current children cumulated vsize (Kb) 53176 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 102823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1029.11 Current children cumulated vsize (Kb) 53176 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 103823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1039.11 Current children cumulated vsize (Kb) 53176 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 104823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1049.11 Current children cumulated vsize (Kb) 53176 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 105823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1059.11 Current children cumulated vsize (Kb) 53176 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 106823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223024 134552020 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1069.11 Current children cumulated vsize (Kb) 53176 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 107823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1079.11 Current children cumulated vsize (Kb) 53176 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 108823 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1089.11 Current children cumulated vsize (Kb) 53176 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12612 0 0 0 109824 87 0 0 25 0 1 0 1783047233 52277248 12598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 12763 12598 145 145 0 12618 0 [pid=9436] vsize: 51052 Current children cumulated CPU time (s) 1099.12 Current children cumulated vsize (Kb) 53176 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 12867 0 0 0 110820 89 0 0 25 0 1 0 1783047233 53350400 12853 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13025 12853 145 145 0 12880 0 [pid=9436] vsize: 52100 Current children cumulated CPU time (s) 1109.1 Current children cumulated vsize (Kb) 54224 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13560 0 0 0 111809 94 0 0 25 0 1 0 1783047233 56225792 13546 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13727 13546 145 145 0 13582 0 [pid=9436] vsize: 54908 Current children cumulated CPU time (s) 1119.04 Current children cumulated vsize (Kb) 57032 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 112809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0 [pid=9436] vsize: 54972 Current children cumulated CPU time (s) 1129.04 Current children cumulated vsize (Kb) 57096 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 113809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0 [pid=9436] vsize: 54972 Current children cumulated CPU time (s) 1139.04 Current children cumulated vsize (Kb) 57096 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13570 0 0 0 114809 94 0 0 25 0 1 0 1783047233 56291328 13556 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13743 13556 145 145 0 13598 0 [pid=9436] vsize: 54972 Current children cumulated CPU time (s) 1149.04 Current children cumulated vsize (Kb) 57096 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 13596 0 0 0 115809 95 0 0 25 0 1 0 1783047233 56455168 13582 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 13783 13582 145 145 0 13638 0 [pid=9436] vsize: 55132 Current children cumulated CPU time (s) 1159.05 Current children cumulated vsize (Kb) 57256 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 14114 0 0 0 116802 97 0 0 25 0 1 0 1783047233 58593280 14100 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 14305 14100 145 145 0 14160 0 [pid=9436] vsize: 57220 Current children cumulated CPU time (s) 1169 Current children cumulated vsize (Kb) 59344 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 14732 0 0 0 117793 102 0 0 25 0 1 0 1783047233 61157376 14718 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 14931 14718 145 145 0 14786 0 [pid=9436] vsize: 59724 Current children cumulated CPU time (s) 1178.96 Current children cumulated vsize (Kb) 61848 [startup+1190.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 15257 0 0 0 118784 105 0 0 25 0 1 0 1783047233 63320064 15243 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 15459 15243 145 145 0 15314 0 [pid=9436] vsize: 61836 Current children cumulated CPU time (s) 1188.9 Current children cumulated vsize (Kb) 63960 [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16036 0 0 0 119773 110 0 0 25 0 1 0 1783047233 66502656 16022 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 16236 16022 145 145 0 16091 0 [pid=9436] vsize: 64944 Current children cumulated CPU time (s) 1198.84 Current children cumulated vsize (Kb) 67068 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16580 0 0 0 120763 114 0 0 25 0 1 0 1783047233 68763648 16566 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 16788 16566 145 145 0 16643 0 [pid=9436] vsize: 67152 Current children cumulated CPU time (s) 1208.78 Current children cumulated vsize (Kb) 69276 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 9436 Raw data (/proc/9432/stat): 9432 (minisat+_script) S 9431 9432 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1783047228 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/9432/statm): 531 226 485 147 0 384 0 [pid=9432] vsize: 2124 Raw data (/proc/9436/stat): 9436 (minisat+_64-bit) R 9432 9432 6847 0 -1 0 16580 0 0 0 120764 114 0 0 25 0 1 0 1783047233 68763648 16566 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/9436/statm): 16788 16566 145 145 0 16643 0 [pid=9436] vsize: 67152 Current children cumulated CPU time (s) 1208.79 Current children cumulated vsize (Kb) 69276 Sending SIGTERM to -9432 Sleeping 2 seconds One traced child (pid=9432) ended because it received signal 15 (SIGTERM) One traced child (pid=9436) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.16 CPU time (s): 1208.81 CPU user time (s): 1207.64 CPU system time (s): 1.17082 CPU usage (%): 99.8883 Max. virtual memory (cumulated for all children) (Kb): 69276
ERROR: no interpretation found !