Name | submitted/aloul/FPGA_SAT05/normalized-chnl50_60_pb.cnf.cr.opb |
MD5SUM | 6968a43b42bba7df68b13fdfd3b616a1 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 61 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.207967 |
Number of variables | 6000 |
Total number of constraints | 220 |
Number of constraints which are clauses | 120 |
Number of constraints which are cardinality constraints (but not clauses) | 100 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 50 |
Maximum length of a constraint | 60 |
LAUNCH ON wulflinc25 THE 2005-09-18 12:30:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2363 boxname=wulflinc25 idbench=19 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6968a43b42bba7df68b13fdfd3b616a1 /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_60_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_60_pb.cnf.cr.opb IDLAUNCH: 2363 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 941848 kB Buffers: 34352 kB Cached: 31596 kB SwapCached: 896 kB Active: 53528 kB Inactive: 15048 kB HighTotal: 131008 kB HighFree: 98028 kB LowTotal: 903652 kB LowFree: 843820 kB SwapTotal: 2097892 kB SwapFree: 2096496 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5716 kB Slab: 18652 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 12:50:20 (client local time) WITH STATUS 0 IN 1207.4 SECONDS stats: 2363 7 1207.4 0
c Parsing PB file... c Converting 220 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................ c ---[ 99]---> BDD-cost: 117 c ---[ 98]---> BDD-cost: 117 c ---[ 97]---> BDD-cost: 117 c ---[ 96]---> BDD-cost: 117 c ---[ 95]---> BDD-cost: 117 c ---[ 94]---> BDD-cost: 117 c ---[ 93]---> BDD-cost: 117 c ---[ 92]---> BDD-cost: 117 c ---[ 91]---> BDD-cost: 117 c ---[ 90]---> BDD-cost: 117 c ---[ 89]---> BDD-cost: 117 c ---[ 88]---> BDD-cost: 117 c ---[ 87]---> BDD-cost: 117 c ---[ 86]---> BDD-cost: 117 c ---[ 85]---> BDD-cost: 117 c ---[ 84]---> BDD-cost: 117 c ---[ 83]---> BDD-cost: 117 c ---[ 82]---> BDD-cost: 117 c ---[ 81]---> BDD-cost: 117 c ---[ 80]---> BDD-cost: 117 c ---[ 79]---> BDD-cost: 117 c ---[ 78]---> BDD-cost: 117 c ---[ 77]---> BDD-cost: 117 c ---[ 76]---> BDD-cost: 117 c ---[ 75]---> BDD-cost: 117 c ---[ 74]---> BDD-cost: 117 c ---[ 73]---> BDD-cost: 117 c ---[ 72]---> BDD-cost: 117 c ---[ 71]---> BDD-cost: 117 c ---[ 70]---> BDD-cost: 117 c ---[ 69]---> BDD-cost: 117 c ---[ 68]---> BDD-cost: 117 c ---[ 67]---> BDD-cost: 117 c ---[ 66]---> BDD-cost: 117 c ---[ 65]---> BDD-cost: 117 c ---[ 64]---> BDD-cost: 117 c ---[ 63]---> BDD-cost: 117 c ---[ 62]---> BDD-cost: 117 c ---[ 61]---> BDD-cost: 117 c ---[ 60]---> BDD-cost: 117 c ---[ 59]---> BDD-cost: 117 c ---[ 58]---> BDD-cost: 117 c ---[ 57]---> BDD-cost: 117 c ---[ 56]---> BDD-cost: 117 c ---[ 55]---> BDD-cost: 117 c ---[ 54]---> BDD-cost: 117 c ---[ 53]---> BDD-cost: 117 c ---[ 52]---> BDD-cost: 117 c ---[ 51]---> BDD-cost: 117 c ---[ 50]---> BDD-cost: 117 c ---[ 49]---> BDD-cost: 117 c ---[ 48]---> BDD-cost: 117 c ---[ 47]---> BDD-cost: 117 c ---[ 46]---> BDD-cost: 117 c ---[ 45]---> BDD-cost: 117 c ---[ 44]---> BDD-cost: 117 c ---[ 43]---> BDD-cost: 117 c ---[ 42]---> BDD-cost: 117 c ---[ 41]---> BDD-cost: 117 c ---[ 40]---> BDD-cost: 117 c ---[ 39]---> BDD-cost: 117 c ---[ 38]---> BDD-cost: 117 c ---[ 37]---> BDD-cost: 117 c ---[ 36]---> BDD-cost: 117 c ---[ 35]---> BDD-cost: 117 c ---[ 34]---> BDD-cost: 117 c ---[ 33]---> BDD-cost: 117 c ---[ 32]---> BDD-cost: 117 c ---[ 31]---> BDD-cost: 117 c ---[ 30]---> BDD-cost: 117 c ---[ 29]---> BDD-cost: 117 c ---[ 28]---> BDD-cost: 117 c ---[ 27]---> BDD-cost: 117 c ---[ 26]---> BDD-cost: 117 c ---[ 25]---> BDD-cost: 117 c ---[ 24]---> BDD-cost: 117 c ---[ 23]---> BDD-cost: 117 c ---[ 22]---> BDD-cost: 117 c ---[ 21]---> BDD-cost: 117 c ---[ 20]---> BDD-cost: 117 c ---[ 19]---> BDD-cost: 117 c ---[ 18]---> BDD-cost: 117 c ---[ 17]---> BDD-cost: 117 c ---[ 16]---> BDD-cost: 117 c ---[ 15]---> BDD-cost: 117 c ---[ 14]---> BDD-cost: 117 c ---[ 13]---> BDD-cost: 117 c ---[ 12]---> BDD-cost: 117 c ---[ 11]---> BDD-cost: 117 c ---[ 10]---> BDD-cost: 117 c ---[ 9]---> BDD-cost: 117 c ---[ 8]---> BDD-cost: 117 c ---[ 7]---> BDD-cost: 117 c ---[ 6]---> BDD-cost: 117 c ---[ 5]---> BDD-cost: 117 c ---[ 4]---> BDD-cost: 117 c ---[ 3]---> BDD-cost: 117 c ---[ 2]---> BDD-cost: 117 c ---[ 1]---> BDD-cost: 117 c ---[ 0]---> BDD-cost: 117 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 29220 81700 | 9740 0 0 nan | 0.000 % | c | 104 | 29220 81700 | 10714 104 19328 185.8 | 0.565 % | c | 256 | 29220 81700 | 11785 256 51373 200.7 | 0.565 % | c | 482 | 29220 81700 | 12963 482 102298 212.2 | 0.565 % | c | 824 | 29220 81700 | 14260 824 174285 211.5 | 0.565 % | c | 1330 | 29220 81700 | 15686 1330 314613 236.6 | 0.565 % | c | 2091 | 29220 81700 | 17255 2091 547467 261.8 | 0.565 % | c | 3231 | 29220 81700 | 18980 3231 973163 301.2 | 0.565 % | c | 4940 | 29220 81700 | 20878 4940 1825691 369.6 | 0.565 % | c | 7502 | 29220 81700 | 22966 7502 3300948 440.0 | 0.565 % | c | 11349 | 29220 81700 | 25263 11349 4927293 434.2 | 0.565 % | c | 17116 | 29220 81700 | 27789 17116 7830885 457.5 | 0.565 % | c | 25776 | 29220 81700 | 30568 25776 12693138 492.4 | 0.565 % | c | 38750 | 29220 81700 | 33625 12745 7008530 549.9 | 0.565 % | c | 58211 | 29220 81700 | 36987 32206 21026723 652.9 | 0.565 % | c | 87408 | 29220 81700 | 40686 27744 13222109 476.6 | 0.565 % | c | 131200 | 29220 81700 | 44755 36115 20717915 573.7 | 0.565 % |
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/6967/stat): 6967 (minisat+_script) R 6966 6967 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1841293566 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/6967/statm): 174 3 169 147 0 27 0 [pid=6967] 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=6968 New process pid=6969 New process pid=6970 execve syscall for /bin/sed executable One traced child (pid=6969) 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=6970) exited with status: 0 One traced child (pid=6968) exited with status: 0 New process pid=6971 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-chnl50_60_pb.cnf.cr.opb [startup+10.0057 s] Raw data (loadavg): 0.93 0.98 0.96 1/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) T 6967 6967 4419 0 -1 0 3358 0 2 0 949 14 0 0 25 0 1 0 1841293571 14512128 3264 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/6971/statm): 3543 3264 145 145 0 3398 0 [pid=6971] vsize: 14172 Current children cumulated CPU time (s) 9.63 Current children cumulated vsize (Kb) 16296 [startup+20.0063 s] Raw data (loadavg): 0.94 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 4962 0 2 0 1929 23 0 0 25 0 1 0 1841293571 21069824 4868 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 5144 4868 145 145 0 4999 0 [pid=6971] vsize: 20576 Current children cumulated CPU time (s) 19.52 Current children cumulated vsize (Kb) 22700 [startup+30.0069 s] Raw data (loadavg): 0.95 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 6556 0 2 0 2908 32 0 0 25 0 1 0 1841293571 27615232 6462 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 6742 6462 145 145 0 6597 0 [pid=6971] vsize: 26968 Current children cumulated CPU time (s) 29.4 Current children cumulated vsize (Kb) 29092 [startup+40.0075 s] Raw data (loadavg): 0.96 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 8026 0 2 0 3888 40 0 0 25 0 1 0 1841293571 33624064 7932 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 8209 7932 145 145 0 8064 0 [pid=6971] vsize: 32836 Current children cumulated CPU time (s) 39.28 Current children cumulated vsize (Kb) 34960 [startup+50.0081 s] Raw data (loadavg): 0.96 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 9463 0 2 0 4868 50 0 0 25 0 1 0 1841293571 39571456 9369 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 9661 9369 145 145 0 9516 0 [pid=6971] vsize: 38644 Current children cumulated CPU time (s) 49.18 Current children cumulated vsize (Kb) 40768 [startup+60.0087 s] Raw data (loadavg): 0.97 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 10820 0 2 0 5847 59 0 0 25 0 1 0 1841293571 45117440 10726 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 11015 10726 145 145 0 10870 0 [pid=6971] vsize: 44060 Current children cumulated CPU time (s) 59.06 Current children cumulated vsize (Kb) 46184 [startup+70.0093 s] Raw data (loadavg): 0.97 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 12236 0 2 0 6829 66 0 0 25 0 1 0 1841293571 50909184 12142 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 12429 12142 145 145 0 12284 0 [pid=6971] vsize: 49716 Current children cumulated CPU time (s) 68.95 Current children cumulated vsize (Kb) 51840 [startup+80.0099 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 13497 0 2 0 7812 73 0 0 25 0 1 0 1841293571 56066048 13403 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 13688 13403 145 145 0 13543 0 [pid=6971] vsize: 54752 Current children cumulated CPU time (s) 78.85 Current children cumulated vsize (Kb) 56876 [startup+90.0105 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 14550 0 2 0 8796 81 0 0 25 0 1 0 1841293571 60375040 14456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 14740 14456 145 145 0 14595 0 [pid=6971] vsize: 58960 Current children cumulated CPU time (s) 88.77 Current children cumulated vsize (Kb) 61084 [startup+100.011 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 16093 0 2 0 9775 90 0 0 25 0 1 0 1841293571 66686976 15999 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 16281 15999 145 145 0 16136 0 [pid=6971] vsize: 65124 Current children cumulated CPU time (s) 98.65 Current children cumulated vsize (Kb) 67248 [startup+110.012 s] Raw data (loadavg): 0.98 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 17557 0 2 0 10754 99 0 0 25 0 1 0 1841293571 72671232 17463 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 17742 17463 145 145 0 17597 0 [pid=6971] vsize: 70968 Current children cumulated CPU time (s) 108.53 Current children cumulated vsize (Kb) 73092 [startup+120.012 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 18682 0 2 0 11736 105 0 0 25 0 1 0 1841293571 77402112 18588 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 18897 18588 145 145 0 18752 0 [pid=6971] vsize: 75588 Current children cumulated CPU time (s) 118.41 Current children cumulated vsize (Kb) 77712 [startup+130.012 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 19671 0 2 0 12720 112 0 0 25 0 1 0 1841293571 81453056 19577 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 19886 19577 145 145 0 19741 0 [pid=6971] vsize: 79544 Current children cumulated CPU time (s) 128.32 Current children cumulated vsize (Kb) 81668 [startup+140.013 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 20454 0 2 0 13708 117 0 0 25 0 1 0 1841293571 84656128 20360 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 20668 20360 145 145 0 20523 0 [pid=6971] vsize: 82672 Current children cumulated CPU time (s) 138.25 Current children cumulated vsize (Kb) 84796 [startup+150.013 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21085 0 2 0 14697 122 0 0 25 0 1 0 1841293571 87244800 20991 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21300 20991 145 145 0 21155 0 [pid=6971] vsize: 85200 Current children cumulated CPU time (s) 148.19 Current children cumulated vsize (Kb) 87324 [startup+160.014 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21688 0 2 0 15688 125 0 0 25 0 1 0 1841293571 89731072 21594 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21907 21594 145 145 0 21762 0 [pid=6971] vsize: 87628 Current children cumulated CPU time (s) 158.13 Current children cumulated vsize (Kb) 89752 [startup+170.014 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 16687 125 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 168.12 Current children cumulated vsize (Kb) 89988 [startup+180.015 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 17686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 178.12 Current children cumulated vsize (Kb) 89988 [startup+190.017 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 18686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 188.12 Current children cumulated vsize (Kb) 89988 [startup+200.017 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 19686 126 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 198.12 Current children cumulated vsize (Kb) 89988 [startup+210.019 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 20685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 208.12 Current children cumulated vsize (Kb) 89988 [startup+220.019 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 21685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 218.12 Current children cumulated vsize (Kb) 89988 [startup+230.02 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 22685 127 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 228.12 Current children cumulated vsize (Kb) 89988 [startup+240.022 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 23684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 238.12 Current children cumulated vsize (Kb) 89988 [startup+250.022 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 24684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 248.12 Current children cumulated vsize (Kb) 89988 [startup+260.024 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21750 0 2 0 25684 128 0 0 25 0 1 0 1841293571 89972736 21656 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 21966 21656 145 145 0 21821 0 [pid=6971] vsize: 87864 Current children cumulated CPU time (s) 258.12 Current children cumulated vsize (Kb) 89988 [startup+270.024 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 21970 0 2 0 26680 131 0 0 25 0 1 0 1841293571 90873856 21876 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 22186 21876 145 145 0 22041 0 [pid=6971] vsize: 88744 Current children cumulated CPU time (s) 268.11 Current children cumulated vsize (Kb) 90868 [startup+280.025 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 23180 0 2 0 27664 137 0 0 25 0 1 0 1841293571 95854592 23086 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 23402 23086 145 145 0 23257 0 [pid=6971] vsize: 93608 Current children cumulated CPU time (s) 278.01 Current children cumulated vsize (Kb) 95732 [startup+290.027 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 24137 0 2 0 28652 143 0 0 25 0 1 0 1841293571 99835904 24043 4294967295 134512640 135094434 3221224432 3221223024 134556993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 24374 24043 145 145 0 24229 0 [pid=6971] vsize: 97496 Current children cumulated CPU time (s) 287.95 Current children cumulated vsize (Kb) 99620 [startup+300.027 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 25438 0 2 0 29632 151 0 0 25 0 1 0 1841293571 105168896 25344 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 25676 25344 145 145 0 25531 0 [pid=6971] vsize: 102704 Current children cumulated CPU time (s) 297.83 Current children cumulated vsize (Kb) 104828 [startup+310.028 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 26369 0 2 0 30617 157 0 0 25 0 1 0 1841293571 108990464 26275 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 26609 26275 145 145 0 26464 0 [pid=6971] vsize: 106436 Current children cumulated CPU time (s) 307.74 Current children cumulated vsize (Kb) 108560 [startup+320.029 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 27173 0 2 0 31605 162 0 0 25 0 1 0 1841293571 112291840 27079 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 27415 27079 145 145 0 27270 0 [pid=6971] vsize: 109660 Current children cumulated CPU time (s) 317.67 Current children cumulated vsize (Kb) 111784 [startup+330.03 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 28024 0 2 0 32591 167 0 0 25 0 1 0 1841293571 115781632 27930 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 28267 27930 145 145 0 28122 0 [pid=6971] vsize: 113068 Current children cumulated CPU time (s) 327.58 Current children cumulated vsize (Kb) 115192 [startup+340.031 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 28758 0 2 0 33579 172 0 0 25 0 1 0 1841293571 118800384 28664 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 29004 28664 145 145 0 28859 0 [pid=6971] vsize: 116016 Current children cumulated CPU time (s) 337.51 Current children cumulated vsize (Kb) 118140 [startup+350.031 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 29487 0 2 0 34570 175 0 0 25 0 1 0 1841293571 121790464 29393 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 29734 29393 145 145 0 29589 0 [pid=6971] vsize: 118936 Current children cumulated CPU time (s) 347.45 Current children cumulated vsize (Kb) 121060 [startup+360.033 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30024 0 2 0 35559 180 0 0 25 0 1 0 1841293571 123981824 29930 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29930 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 357.39 Current children cumulated vsize (Kb) 123200 [startup+370.033 s] Raw data (loadavg): 0.99 0.98 0.96 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30024 0 2 0 36559 180 0 0 25 0 1 0 1841293571 123981824 29930 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29930 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 367.39 Current children cumulated vsize (Kb) 123200 [startup+380.034 s] Raw data (loadavg): 1.07 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 37559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 377.4 Current children cumulated vsize (Kb) 123200 [startup+390.036 s] Raw data (loadavg): 1.06 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 38559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 387.4 Current children cumulated vsize (Kb) 123200 [startup+400.036 s] Raw data (loadavg): 1.05 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 39559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 397.4 Current children cumulated vsize (Kb) 123200 [startup+410.037 s] Raw data (loadavg): 1.04 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30025 0 2 0 40559 181 0 0 25 0 1 0 1841293571 123981824 29931 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29931 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 407.4 Current children cumulated vsize (Kb) 123200 [startup+420.038 s] Raw data (loadavg): 1.04 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 41559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 417.41 Current children cumulated vsize (Kb) 123200 [startup+430.038 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 42559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 427.41 Current children cumulated vsize (Kb) 123200 [startup+440.039 s] Raw data (loadavg): 1.03 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 43559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 437.41 Current children cumulated vsize (Kb) 123200 [startup+450.039 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 44559 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 447.41 Current children cumulated vsize (Kb) 123200 [startup+460.04 s] Raw data (loadavg): 1.02 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 45560 182 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 457.42 Current children cumulated vsize (Kb) 123200 [startup+470.04 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 46559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 467.42 Current children cumulated vsize (Kb) 123200 [startup+480.041 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 47559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 477.42 Current children cumulated vsize (Kb) 123200 [startup+490.042 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 48559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 487.42 Current children cumulated vsize (Kb) 123200 [startup+500.042 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 49559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 497.42 Current children cumulated vsize (Kb) 123200 [startup+510.042 s] Raw data (loadavg): 1.01 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 50559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223024 134556791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 507.42 Current children cumulated vsize (Kb) 123200 [startup+520.042 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 51559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 517.42 Current children cumulated vsize (Kb) 123200 [startup+530.043 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 52560 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 527.43 Current children cumulated vsize (Kb) 123200 [startup+540.044 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30027 0 2 0 53559 183 0 0 25 0 1 0 1841293571 123981824 29933 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29933 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 537.42 Current children cumulated vsize (Kb) 123200 [startup+550.044 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30028 0 2 0 54560 183 0 0 25 0 1 0 1841293571 123981824 29934 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29934 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 547.43 Current children cumulated vsize (Kb) 123200 [startup+560.045 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 55560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223104 134555967 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 557.43 Current children cumulated vsize (Kb) 123200 [startup+570.045 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 56560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 567.43 Current children cumulated vsize (Kb) 123200 [startup+580.045 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 57560 183 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 577.43 Current children cumulated vsize (Kb) 123200 [startup+590.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 58560 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 587.44 Current children cumulated vsize (Kb) 123200 [startup+600.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 59560 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 597.44 Current children cumulated vsize (Kb) 123200 [startup+610.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 60561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 607.45 Current children cumulated vsize (Kb) 123200 [startup+620.046 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 61561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 617.45 Current children cumulated vsize (Kb) 123200 [startup+630.047 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 62561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 627.45 Current children cumulated vsize (Kb) 123200 [startup+640.048 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 63561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 637.45 Current children cumulated vsize (Kb) 123200 [startup+650.048 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 64561 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 647.45 Current children cumulated vsize (Kb) 123200 [startup+660.049 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 65562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 657.46 Current children cumulated vsize (Kb) 123200 [startup+670.049 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 66562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 667.46 Current children cumulated vsize (Kb) 123200 [startup+680.05 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 67562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 677.46 Current children cumulated vsize (Kb) 123200 [startup+690.051 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 68562 184 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 687.46 Current children cumulated vsize (Kb) 123200 [startup+700.051 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 69562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 697.47 Current children cumulated vsize (Kb) 123200 [startup+710.052 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 70562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 707.47 Current children cumulated vsize (Kb) 123200 [startup+720.053 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 71562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 717.47 Current children cumulated vsize (Kb) 123200 [startup+730.053 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 72562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 727.47 Current children cumulated vsize (Kb) 123200 [startup+740.054 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 73562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 737.47 Current children cumulated vsize (Kb) 123200 [startup+750.054 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 74562 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 747.47 Current children cumulated vsize (Kb) 123200 [startup+760.054 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 75563 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 757.48 Current children cumulated vsize (Kb) 123200 [startup+770.054 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30029 0 2 0 76563 185 0 0 25 0 1 0 1841293571 123981824 29935 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30269 29935 145 145 0 30124 0 [pid=6971] vsize: 121076 Current children cumulated CPU time (s) 767.48 Current children cumulated vsize (Kb) 123200 [startup+780.055 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 30498 0 2 0 77557 187 0 0 25 0 1 0 1841293571 125906944 30404 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 30739 30404 145 145 0 30594 0 [pid=6971] vsize: 122956 Current children cumulated CPU time (s) 777.44 Current children cumulated vsize (Kb) 125080 [startup+790.056 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 31241 0 2 0 78544 192 0 0 25 0 1 0 1841293571 128950272 31147 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 31482 31147 145 145 0 31337 0 [pid=6971] vsize: 125928 Current children cumulated CPU time (s) 787.36 Current children cumulated vsize (Kb) 128052 [startup+800.056 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 31906 0 2 0 79534 196 0 0 25 0 1 0 1841293571 131686400 31812 4294967295 134512640 135094434 3221224432 3221223168 134559697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32150 31812 145 145 0 32005 0 [pid=6971] vsize: 128600 Current children cumulated CPU time (s) 797.3 Current children cumulated vsize (Kb) 130724 [startup+810.056 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 80524 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 807.23 Current children cumulated vsize (Kb) 133308 [startup+820.057 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 81525 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 817.24 Current children cumulated vsize (Kb) 133308 [startup+830.057 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 82525 199 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 827.24 Current children cumulated vsize (Kb) 133308 [startup+840.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 83525 200 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 837.25 Current children cumulated vsize (Kb) 133308 [startup+850.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32550 0 2 0 84525 200 0 0 25 0 1 0 1841293571 134332416 32456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32456 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 847.25 Current children cumulated vsize (Kb) 133308 [startup+860.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 85525 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 857.25 Current children cumulated vsize (Kb) 133308 [startup+870.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 86525 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223024 134556757 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 867.25 Current children cumulated vsize (Kb) 133308 [startup+880.059 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 87526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 877.26 Current children cumulated vsize (Kb) 133308 [startup+890.06 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 88526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 887.26 Current children cumulated vsize (Kb) 133308 [startup+900.06 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32552 0 2 0 89526 200 0 0 25 0 1 0 1841293571 134332416 32458 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32458 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 897.26 Current children cumulated vsize (Kb) 133308 [startup+910.061 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 90526 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 907.26 Current children cumulated vsize (Kb) 133308 [startup+920.062 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 91527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 917.27 Current children cumulated vsize (Kb) 133308 [startup+930.062 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 92527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134557256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 927.27 Current children cumulated vsize (Kb) 133308 [startup+940.063 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 93527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 937.27 Current children cumulated vsize (Kb) 133308 [startup+950.063 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 94527 200 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 947.27 Current children cumulated vsize (Kb) 133308 [startup+960.064 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 95525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 957.27 Current children cumulated vsize (Kb) 133308 [startup+970.065 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 96525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 967.27 Current children cumulated vsize (Kb) 133308 [startup+980.065 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 97525 202 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 977.27 Current children cumulated vsize (Kb) 133308 [startup+990.066 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 98525 203 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 987.28 Current children cumulated vsize (Kb) 133308 [startup+1000.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32553 0 2 0 99525 203 0 0 25 0 1 0 1841293571 134332416 32459 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32459 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 997.28 Current children cumulated vsize (Kb) 133308 [startup+1010.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 100525 203 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1007.28 Current children cumulated vsize (Kb) 133308 [startup+1020.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 101525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1017.29 Current children cumulated vsize (Kb) 133308 [startup+1030.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 102525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1027.29 Current children cumulated vsize (Kb) 133308 [startup+1040.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 103525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1037.29 Current children cumulated vsize (Kb) 133308 [startup+1050.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 104525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1047.29 Current children cumulated vsize (Kb) 133308 [startup+1060.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32554 0 2 0 105525 204 0 0 25 0 1 0 1841293571 134332416 32460 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32460 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1057.29 Current children cumulated vsize (Kb) 133308 [startup+1070.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 106525 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1067.29 Current children cumulated vsize (Kb) 133308 [startup+1080.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 107525 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1077.29 Current children cumulated vsize (Kb) 133308 [startup+1090.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 108526 204 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1087.3 Current children cumulated vsize (Kb) 133308 [startup+1100.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 109526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1097.31 Current children cumulated vsize (Kb) 133308 [startup+1110.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 110526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1107.31 Current children cumulated vsize (Kb) 133308 [startup+1120.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 111526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1117.31 Current children cumulated vsize (Kb) 133308 [startup+1130.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 112526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1127.31 Current children cumulated vsize (Kb) 133308 [startup+1140.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 113526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1137.31 Current children cumulated vsize (Kb) 133308 [startup+1150.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32555 0 2 0 114526 205 0 0 25 0 1 0 1841293571 134332416 32461 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32461 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1147.31 Current children cumulated vsize (Kb) 133308 [startup+1160.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 115527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1157.32 Current children cumulated vsize (Kb) 133308 [startup+1170.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 116527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1167.32 Current children cumulated vsize (Kb) 133308 [startup+1180.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 117527 205 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1177.32 Current children cumulated vsize (Kb) 133308 [startup+1190.07 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32556 0 2 0 118527 206 0 0 25 0 1 0 1841293571 134332416 32462 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32462 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1187.33 Current children cumulated vsize (Kb) 133308 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 119527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1197.33 Current children cumulated vsize (Kb) 133308 [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 120527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1207.33 Current children cumulated vsize (Kb) 133308 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.97 2/57 6971 Raw data (/proc/6967/stat): 6967 (minisat+_script) S 6966 6967 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1841293566 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/6967/statm): 531 226 485 147 0 384 0 [pid=6967] vsize: 2124 Raw data (/proc/6971/stat): 6971 (minisat+_64-bit) R 6967 6967 4419 0 -1 0 32557 0 2 0 120527 206 0 0 25 0 1 0 1841293571 134332416 32463 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/6971/statm): 32796 32463 145 145 0 32651 0 [pid=6971] vsize: 131184 Current children cumulated CPU time (s) 1207.33 Current children cumulated vsize (Kb) 133308 Sending SIGTERM to -6967 Sleeping 2 seconds One traced child (pid=6967) ended because it received signal 15 (SIGTERM) One traced child (pid=6971) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.14 CPU time (s): 1207.4 CPU user time (s): 1205.28 CPU system time (s): 2.12168 CPU usage (%): 99.7738 Max. virtual memory (cumulated for all children) (Kb): 133308
ERROR: no interpretation found !