Name | submitted/aloul/FPGA_SAT05/normalized-chnl30_31_pb.cnf.cr.opb |
MD5SUM | 79bafd08ddd684356ab9abc8fabf88a7 |
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 | 32 |
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.05899 |
Number of variables | 1860 |
Total number of constraints | 122 |
Number of constraints which are clauses | 62 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 31 |
LAUNCH ON wulflinc11 THE 2005-09-18 12:24:07 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2353 boxname=wulflinc11 idbench=9 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 79bafd08ddd684356ab9abc8fabf88a7 /oldhome/oroussel/tmp/wulflinc11/normalized-chnl30_31_pb.cnf.cr.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-chnl30_31_pb.cnf.cr.opb IDLAUNCH: 2353 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 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 : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 958348 kB Buffers: 23496 kB Cached: 25684 kB SwapCached: 732 kB Active: 12336 kB Inactive: 39372 kB HighTotal: 131008 kB HighFree: 103488 kB LowTotal: 903652 kB LowFree: 854860 kB SwapTotal: 2097136 kB SwapFree: 2095856 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 18848 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 12:44:17 (client local time) WITH STATUS 0 IN 1208.88 SECONDS stats: 2353 7 1208.88 0
c Parsing PB file... c Converting 122 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................. c ---[ 59]---> BDD-cost: 59 c ---[ 58]---> BDD-cost: 59 c ---[ 57]---> BDD-cost: 59 c ---[ 56]---> BDD-cost: 59 c ---[ 55]---> BDD-cost: 59 c ---[ 54]---> BDD-cost: 59 c ---[ 53]---> BDD-cost: 59 c ---[ 52]---> BDD-cost: 59 c ---[ 51]---> BDD-cost: 59 c ---[ 50]---> BDD-cost: 59 c ---[ 49]---> BDD-cost: 59 c ---[ 48]---> BDD-cost: 59 c ---[ 47]---> BDD-cost: 59 c ---[ 46]---> BDD-cost: 59 c ---[ 45]---> BDD-cost: 59 c ---[ 44]---> BDD-cost: 59 c ---[ 43]---> BDD-cost: 59 c ---[ 42]---> BDD-cost: 59 c ---[ 41]---> BDD-cost: 59 c ---[ 40]---> BDD-cost: 59 c ---[ 39]---> BDD-cost: 59 c ---[ 38]---> BDD-cost: 59 c ---[ 37]---> BDD-cost: 59 c ---[ 36]---> BDD-cost: 59 c ---[ 35]---> BDD-cost: 59 c ---[ 34]---> BDD-cost: 59 c ---[ 33]---> BDD-cost: 59 c ---[ 32]---> BDD-cost: 59 c ---[ 31]---> BDD-cost: 59 c ---[ 30]---> BDD-cost: 59 c ---[ 29]---> BDD-cost: 59 c ---[ 28]---> BDD-cost: 59 c ---[ 27]---> BDD-cost: 59 c ---[ 26]---> BDD-cost: 59 c ---[ 25]---> BDD-cost: 59 c ---[ 24]---> BDD-cost: 59 c ---[ 23]---> BDD-cost: 59 c ---[ 22]---> BDD-cost: 59 c ---[ 21]---> BDD-cost: 59 c ---[ 20]---> BDD-cost: 59 c ---[ 19]---> BDD-cost: 59 c ---[ 18]---> BDD-cost: 59 c ---[ 17]---> BDD-cost: 59 c ---[ 16]---> BDD-cost: 59 c ---[ 15]---> BDD-cost: 59 c ---[ 14]---> BDD-cost: 59 c ---[ 13]---> BDD-cost: 59 c ---[ 12]---> BDD-cost: 59 c ---[ 11]---> BDD-cost: 59 c ---[ 10]---> BDD-cost: 59 c ---[ 9]---> BDD-cost: 59 c ---[ 8]---> BDD-cost: 59 c ---[ 7]---> BDD-cost: 59 c ---[ 6]---> BDD-cost: 59 c ---[ 5]---> BDD-cost: 59 c ---[ 4]---> BDD-cost: 59 c ---[ 3]---> BDD-cost: 59 c ---[ 2]---> BDD-cost: 59 c ---[ 1]---> BDD-cost: 59 c ---[ 0]---> BDD-cost: 59 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 8822 24660 | 2940 0 0 nan | 0.000 % | c | 103 | 8822 24660 | 3234 103 11125 108.0 | 1.111 % | c | 253 | 8822 24660 | 3557 253 29108 115.1 | 1.111 % | c | 481 | 8822 24660 | 3913 481 60948 126.7 | 1.111 % | c | 818 | 8822 24660 | 4304 818 108840 133.1 | 1.111 % | c | 1324 | 8822 24660 | 4734 1324 188898 142.7 | 1.111 % | c | 2083 | 8822 24660 | 5208 2083 314214 150.8 | 1.111 % | c | 3222 | 8822 24660 | 5729 3222 492986 153.0 | 1.111 % | c | 4931 | 8822 24660 | 6302 4931 860748 174.6 | 1.111 % | c | 7493 | 8822 24660 | 6932 4279 864687 202.1 | 1.111 % | c | 11338 | 8822 24660 | 7625 8124 1810763 222.9 | 1.111 % | c | 17104 | 8822 24660 | 8388 4954 1245773 251.5 | 1.111 % | c | 25753 | 8822 24660 | 9226 8309 2172756 261.5 | 1.111 % | c | 38729 | 8822 24660 | 10149 10285 3566365 346.8 | 1.111 % | c | 58191 | 8822 24660 | 11164 6370 1674827 262.9 | 1.111 % | c | 87385 | 8822 24660 | 12281 8866 2685374 302.9 | 1.111 % | c | 131174 | 8822 24660 | 13509 10011 3644159 364.0 | 1.111 % | c | 196858 | 8822 24660 | 14860 16739 4896164 292.5 | 1.111 % | c | 295385 | 8822 24660 | 16346 15539 3921113 252.3 | 1.111 % |
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/12306/stat): 12306 (minisat+_script) R 12305 12306 9854 0 -1 0 18 0 1 0 0 0 0 0 22 0 1 0 1782998956 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/12306/statm): 174 3 169 147 0 27 0 [pid=12306] 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=12307 New process pid=12308 New process pid=12309 One traced child (pid=12308) exited with status: 0 execve syscall for /bin/sed executable 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=12309) exited with status: 0 One traced child (pid=12307) exited with status: 0 New process pid=12310 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-chnl30_31_pb.cnf.cr.opb [startup+10.0072 s] Raw data (loadavg): 0.94 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 2222 0 2 0 950 10 0 0 25 0 1 0 1782998965 9494528 2211 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 2318 2211 145 145 0 2173 0 [pid=12310] vsize: 9272 Current children cumulated CPU time (s) 9.62 Current children cumulated vsize (Kb) 11396 [startup+20.0081 s] Raw data (loadavg): 0.95 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 3236 0 2 0 1935 17 0 0 25 0 1 0 1782998965 13672448 3225 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 3338 3225 145 145 0 3193 0 [pid=12310] vsize: 13352 Current children cumulated CPU time (s) 19.54 Current children cumulated vsize (Kb) 15476 [startup+30.0098 s] Raw data (loadavg): 0.95 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 3533 0 2 0 2930 19 0 0 25 0 1 0 1782998965 14888960 3522 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 3635 3522 145 145 0 3490 0 [pid=12310] vsize: 14540 Current children cumulated CPU time (s) 29.51 Current children cumulated vsize (Kb) 16664 [startup+40.0106 s] Raw data (loadavg): 0.96 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 3534 0 2 0 3930 19 0 0 25 0 1 0 1782998965 14888960 3523 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 3635 3523 145 145 0 3490 0 [pid=12310] vsize: 14540 Current children cumulated CPU time (s) 39.51 Current children cumulated vsize (Kb) 16664 [startup+50.0124 s] Raw data (loadavg): 0.97 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4352 0 2 0 4921 23 0 0 25 0 1 0 1782998965 18235392 4341 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4452 4341 145 145 0 4307 0 [pid=12310] vsize: 17808 Current children cumulated CPU time (s) 49.46 Current children cumulated vsize (Kb) 19932 [startup+60.0132 s] Raw data (loadavg): 0.97 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4645 0 2 0 5917 25 0 0 25 0 1 0 1782998965 19435520 4634 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4745 4634 145 145 0 4600 0 [pid=12310] vsize: 18980 Current children cumulated CPU time (s) 59.44 Current children cumulated vsize (Kb) 21104 [startup+70.014 s] Raw data (loadavg): 0.97 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4706 0 2 0 6915 26 0 0 25 0 1 0 1782998965 19685376 4695 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4806 4695 145 145 0 4661 0 [pid=12310] vsize: 19224 Current children cumulated CPU time (s) 69.43 Current children cumulated vsize (Kb) 21348 [startup+80.0158 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4811 0 2 0 7914 27 0 0 25 0 1 0 1782998965 20127744 4800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4914 4800 145 145 0 4769 0 [pid=12310] vsize: 19656 Current children cumulated CPU time (s) 79.43 Current children cumulated vsize (Kb) 21780 [startup+90.0166 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4811 0 2 0 8913 27 0 0 25 0 1 0 1782998965 20127744 4800 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4914 4800 145 145 0 4769 0 [pid=12310] vsize: 19656 Current children cumulated CPU time (s) 89.42 Current children cumulated vsize (Kb) 21780 [startup+100.018 s] Raw data (loadavg): 0.98 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4811 0 2 0 9913 27 0 0 25 0 1 0 1782998965 20127744 4800 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4914 4800 145 145 0 4769 0 [pid=12310] vsize: 19656 Current children cumulated CPU time (s) 99.42 Current children cumulated vsize (Kb) 21780 [startup+110.019 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4811 0 2 0 10912 28 0 0 25 0 1 0 1782998965 20127744 4800 4294967295 134512640 135094434 3221224432 3221223024 134557236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 4914 4800 145 145 0 4769 0 [pid=12310] vsize: 19656 Current children cumulated CPU time (s) 109.42 Current children cumulated vsize (Kb) 21780 [startup+120.02 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 4993 0 2 0 11909 29 0 0 25 0 1 0 1782998965 20889600 4982 4294967295 134512640 135094434 3221224432 3221222896 134781325 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5100 4982 145 145 0 4955 0 [pid=12310] vsize: 20400 Current children cumulated CPU time (s) 119.4 Current children cumulated vsize (Kb) 22524 [startup+130.022 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 5148 0 2 0 12906 30 0 0 25 0 1 0 1782998965 21544960 5137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5260 5137 145 145 0 5115 0 [pid=12310] vsize: 21040 Current children cumulated CPU time (s) 129.38 Current children cumulated vsize (Kb) 23164 [startup+140.023 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 5148 0 2 0 13906 30 0 0 25 0 1 0 1782998965 21544960 5137 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5260 5137 145 145 0 5115 0 [pid=12310] vsize: 21040 Current children cumulated CPU time (s) 139.38 Current children cumulated vsize (Kb) 23164 [startup+150.024 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 5363 0 2 0 14903 32 0 0 25 0 1 0 1782998965 22536192 5352 4294967295 134512640 135094434 3221224432 3221223104 134556519 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5502 5352 145 145 0 5357 0 [pid=12310] vsize: 22008 Current children cumulated CPU time (s) 149.37 Current children cumulated vsize (Kb) 24132 [startup+160.025 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 5408 0 2 0 15902 33 0 0 25 0 1 0 1782998965 22716416 5397 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5546 5397 145 145 0 5401 0 [pid=12310] vsize: 22184 Current children cumulated CPU time (s) 159.37 Current children cumulated vsize (Kb) 24308 [startup+170.026 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 5601 0 2 0 16900 34 0 0 25 0 1 0 1782998965 23506944 5590 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 5739 5590 145 145 0 5594 0 [pid=12310] vsize: 22956 Current children cumulated CPU time (s) 169.36 Current children cumulated vsize (Kb) 25080 [startup+180.027 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 6251 0 2 0 17891 38 0 0 25 0 1 0 1782998965 26165248 6240 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 6388 6240 145 145 0 6243 0 [pid=12310] vsize: 25552 Current children cumulated CPU time (s) 179.31 Current children cumulated vsize (Kb) 27676 [startup+190.027 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 7156 0 2 0 18877 44 0 0 25 0 1 0 1782998965 29876224 7145 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 7294 7145 145 145 0 7149 0 [pid=12310] vsize: 29176 Current children cumulated CPU time (s) 189.23 Current children cumulated vsize (Kb) 31300 [startup+200.028 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 7880 0 2 0 19867 49 0 0 25 0 1 0 1782998965 32870400 7869 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 8025 7869 145 145 0 7880 0 [pid=12310] vsize: 32100 Current children cumulated CPU time (s) 199.18 Current children cumulated vsize (Kb) 34224 [startup+210.03 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 7881 0 2 0 20866 50 0 0 25 0 1 0 1782998965 32870400 7870 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8025 7870 145 145 0 7880 0 [pid=12310] vsize: 32100 Current children cumulated CPU time (s) 209.18 Current children cumulated vsize (Kb) 34224 [startup+220.031 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8548 0 2 0 21856 54 0 0 17 0 1 0 1782998965 35643392 8537 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 8702 8537 145 145 0 8557 0 [pid=12310] vsize: 34808 Current children cumulated CPU time (s) 219.12 Current children cumulated vsize (Kb) 36932 [startup+230.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 22852 56 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 229.1 Current children cumulated vsize (Kb) 37700 [startup+240.032 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 23851 56 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 239.09 Current children cumulated vsize (Kb) 37700 [startup+250.033 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 24851 56 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 249.09 Current children cumulated vsize (Kb) 37700 [startup+260.034 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 25851 57 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 259.1 Current children cumulated vsize (Kb) 37700 [startup+270.035 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 26851 57 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 269.1 Current children cumulated vsize (Kb) 37700 [startup+280.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8734 0 2 0 27852 57 0 0 25 0 1 0 1782998965 36429824 8723 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8723 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 279.11 Current children cumulated vsize (Kb) 37700 [startup+290.036 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 28852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 289.11 Current children cumulated vsize (Kb) 37700 [startup+300.037 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 29852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 299.11 Current children cumulated vsize (Kb) 37700 [startup+310.038 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 30852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 309.11 Current children cumulated vsize (Kb) 37700 [startup+320.038 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 31852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 319.11 Current children cumulated vsize (Kb) 37700 [startup+330.039 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 32852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 329.11 Current children cumulated vsize (Kb) 37700 [startup+340.04 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 33852 57 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 339.11 Current children cumulated vsize (Kb) 37700 [startup+350.041 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 34852 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 349.12 Current children cumulated vsize (Kb) 37700 [startup+360.042 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 35853 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 359.13 Current children cumulated vsize (Kb) 37700 [startup+370.043 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 36853 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 369.13 Current children cumulated vsize (Kb) 37700 [startup+380.043 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 37853 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 379.13 Current children cumulated vsize (Kb) 37700 [startup+390.044 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 38853 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223024 134552006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 389.13 Current children cumulated vsize (Kb) 37700 [startup+400.045 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 39853 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 399.13 Current children cumulated vsize (Kb) 37700 [startup+410.046 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 40854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 409.14 Current children cumulated vsize (Kb) 37700 [startup+420.047 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 41854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 419.14 Current children cumulated vsize (Kb) 37700 [startup+430.048 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 42854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 429.14 Current children cumulated vsize (Kb) 37700 [startup+440.049 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 43854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 439.14 Current children cumulated vsize (Kb) 37700 [startup+450.05 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 44854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 449.14 Current children cumulated vsize (Kb) 37700 [startup+460.051 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 45854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 459.14 Current children cumulated vsize (Kb) 37700 [startup+470.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 46854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 469.14 Current children cumulated vsize (Kb) 37700 [startup+480.052 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 8735 0 2 0 47854 58 0 0 25 0 1 0 1782998965 36429824 8724 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 8894 8724 145 145 0 8749 0 [pid=12310] vsize: 35576 Current children cumulated CPU time (s) 479.14 Current children cumulated vsize (Kb) 37700 [startup+490.053 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 9119 0 2 0 48849 61 0 0 25 0 1 0 1782998965 38002688 9108 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 9278 9108 145 145 0 9133 0 [pid=12310] vsize: 37112 Current children cumulated CPU time (s) 489.12 Current children cumulated vsize (Kb) 39236 [startup+500.054 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 9119 0 2 0 49849 61 0 0 25 0 1 0 1782998965 38002688 9108 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 9278 9108 145 145 0 9133 0 [pid=12310] vsize: 37112 Current children cumulated CPU time (s) 499.12 Current children cumulated vsize (Kb) 39236 [startup+510.055 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 9367 0 2 0 50846 62 0 0 25 0 1 0 1782998965 39018496 9356 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 9526 9356 145 145 0 9381 0 [pid=12310] vsize: 38104 Current children cumulated CPU time (s) 509.1 Current children cumulated vsize (Kb) 40228 [startup+520.056 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 10489 0 2 0 51830 68 0 0 25 0 1 0 1782998965 43626496 10478 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 10651 10478 145 145 0 10506 0 [pid=12310] vsize: 42604 Current children cumulated CPU time (s) 519 Current children cumulated vsize (Kb) 44728 [startup+530.056 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 10489 0 2 0 52830 68 0 0 25 0 1 0 1782998965 43626496 10478 4294967295 134512640 135094434 3221224432 3221223104 134555453 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 10651 10478 145 145 0 10506 0 [pid=12310] vsize: 42604 Current children cumulated CPU time (s) 529 Current children cumulated vsize (Kb) 44728 [startup+540.057 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 10489 0 2 0 53831 69 0 0 25 0 1 0 1782998965 43626496 10478 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 10651 10478 145 145 0 10506 0 [pid=12310] vsize: 42604 Current children cumulated CPU time (s) 539.02 Current children cumulated vsize (Kb) 44728 [startup+550.057 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11257 0 2 0 54819 74 0 0 25 0 1 0 1782998965 46788608 11246 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11423 11246 145 145 0 11278 0 [pid=12310] vsize: 45692 Current children cumulated CPU time (s) 548.95 Current children cumulated vsize (Kb) 47816 [startup+560.058 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11257 0 2 0 55819 74 0 0 25 0 1 0 1782998965 46788608 11246 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11423 11246 145 145 0 11278 0 [pid=12310] vsize: 45692 Current children cumulated CPU time (s) 558.95 Current children cumulated vsize (Kb) 47816 [startup+570.058 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11257 0 2 0 56819 74 0 0 25 0 1 0 1782998965 46788608 11246 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11423 11246 145 145 0 11278 0 [pid=12310] vsize: 45692 Current children cumulated CPU time (s) 568.95 Current children cumulated vsize (Kb) 47816 [startup+580.059 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11257 0 2 0 57819 74 0 0 25 0 1 0 1782998965 46788608 11246 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11423 11246 145 145 0 11278 0 [pid=12310] vsize: 45692 Current children cumulated CPU time (s) 578.95 Current children cumulated vsize (Kb) 47816 [startup+590.06 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11257 0 2 0 58820 74 0 0 25 0 1 0 1782998965 46788608 11246 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11423 11246 145 145 0 11278 0 [pid=12310] vsize: 45692 Current children cumulated CPU time (s) 588.96 Current children cumulated vsize (Kb) 47816 [startup+600.061 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 59819 74 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 598.95 Current children cumulated vsize (Kb) 48108 [startup+610.062 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 60819 74 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 608.95 Current children cumulated vsize (Kb) 48108 [startup+620.061 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 61819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 618.96 Current children cumulated vsize (Kb) 48108 [startup+630.062 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 62819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 628.96 Current children cumulated vsize (Kb) 48108 [startup+640.063 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 63819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 638.96 Current children cumulated vsize (Kb) 48108 [startup+650.063 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 64819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 648.96 Current children cumulated vsize (Kb) 48108 [startup+660.064 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 65819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 658.96 Current children cumulated vsize (Kb) 48108 [startup+670.064 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11331 0 2 0 66819 75 0 0 25 0 1 0 1782998965 47087616 11320 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11496 11320 145 145 0 11351 0 [pid=12310] vsize: 45984 Current children cumulated CPU time (s) 668.96 Current children cumulated vsize (Kb) 48108 [startup+680.065 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11417 0 2 0 67818 75 0 0 25 0 1 0 1782998965 47439872 11406 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11582 11406 145 145 0 11437 0 [pid=12310] vsize: 46328 Current children cumulated CPU time (s) 678.95 Current children cumulated vsize (Kb) 48452 [startup+690.066 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11417 0 2 0 68818 75 0 0 25 0 1 0 1782998965 47439872 11406 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11582 11406 145 145 0 11437 0 [pid=12310] vsize: 46328 Current children cumulated CPU time (s) 688.95 Current children cumulated vsize (Kb) 48452 [startup+700.067 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11417 0 2 0 69818 75 0 0 25 0 1 0 1782998965 47439872 11406 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11582 11406 145 145 0 11437 0 [pid=12310] vsize: 46328 Current children cumulated CPU time (s) 698.95 Current children cumulated vsize (Kb) 48452 [startup+710.067 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11655 0 2 0 70814 77 0 0 25 0 1 0 1782998965 48414720 11644 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11820 11644 145 145 0 11675 0 [pid=12310] vsize: 47280 Current children cumulated CPU time (s) 708.93 Current children cumulated vsize (Kb) 49404 [startup+720.067 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11655 0 2 0 71814 77 0 0 25 0 1 0 1782998965 48414720 11644 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11820 11644 145 145 0 11675 0 [pid=12310] vsize: 47280 Current children cumulated CPU time (s) 718.93 Current children cumulated vsize (Kb) 49404 [startup+730.068 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11655 0 2 0 72815 77 0 0 25 0 1 0 1782998965 48414720 11644 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11820 11644 145 145 0 11675 0 [pid=12310] vsize: 47280 Current children cumulated CPU time (s) 728.94 Current children cumulated vsize (Kb) 49404 [startup+740.069 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11655 0 2 0 73815 77 0 0 25 0 1 0 1782998965 48414720 11644 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11820 11644 145 145 0 11675 0 [pid=12310] vsize: 47280 Current children cumulated CPU time (s) 738.94 Current children cumulated vsize (Kb) 49404 [startup+750.069 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11655 0 2 0 74815 77 0 0 25 0 1 0 1782998965 48414720 11644 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11820 11644 145 145 0 11675 0 [pid=12310] vsize: 47280 Current children cumulated CPU time (s) 748.94 Current children cumulated vsize (Kb) 49404 [startup+760.069 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11737 0 2 0 75814 77 0 0 25 0 1 0 1782998965 48750592 11726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11902 11726 145 145 0 11757 0 [pid=12310] vsize: 47608 Current children cumulated CPU time (s) 758.93 Current children cumulated vsize (Kb) 49732 [startup+770.07 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11737 0 2 0 76814 77 0 0 25 0 1 0 1782998965 48750592 11726 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11902 11726 145 145 0 11757 0 [pid=12310] vsize: 47608 Current children cumulated CPU time (s) 768.93 Current children cumulated vsize (Kb) 49732 [startup+780.071 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11737 0 2 0 77814 78 0 0 25 0 1 0 1782998965 48750592 11726 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11902 11726 145 145 0 11757 0 [pid=12310] vsize: 47608 Current children cumulated CPU time (s) 778.94 Current children cumulated vsize (Kb) 49732 [startup+790.072 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 11789 0 2 0 78814 78 0 0 25 0 1 0 1782998965 48984064 11778 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 11959 11778 145 145 0 11814 0 [pid=12310] vsize: 47836 Current children cumulated CPU time (s) 788.94 Current children cumulated vsize (Kb) 49960 [startup+800.072 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 79810 80 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 798.92 Current children cumulated vsize (Kb) 51056 [startup+810.072 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 80809 81 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 808.92 Current children cumulated vsize (Kb) 51056 [startup+820.073 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 81809 81 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 818.92 Current children cumulated vsize (Kb) 51056 [startup+830.074 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 82808 82 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134556966 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 828.92 Current children cumulated vsize (Kb) 51056 [startup+840.075 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 83808 82 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 838.92 Current children cumulated vsize (Kb) 51056 [startup+850.075 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 84808 82 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 848.92 Current children cumulated vsize (Kb) 51056 [startup+860.075 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 85808 82 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 858.92 Current children cumulated vsize (Kb) 51056 [startup+870.076 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 86808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 868.93 Current children cumulated vsize (Kb) 51056 [startup+880.078 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 87808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 878.93 Current children cumulated vsize (Kb) 51056 [startup+890.079 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 88808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 888.93 Current children cumulated vsize (Kb) 51056 [startup+900.079 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 89808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 898.93 Current children cumulated vsize (Kb) 51056 [startup+910.079 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 90808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 908.93 Current children cumulated vsize (Kb) 51056 [startup+920.079 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 91808 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 918.93 Current children cumulated vsize (Kb) 51056 [startup+930.08 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 92809 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 928.94 Current children cumulated vsize (Kb) 51056 [startup+940.081 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 93809 83 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 938.94 Current children cumulated vsize (Kb) 51056 [startup+950.082 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 94809 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 948.95 Current children cumulated vsize (Kb) 51056 [startup+960.082 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 95809 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 958.95 Current children cumulated vsize (Kb) 51056 [startup+970.083 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 96809 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 968.95 Current children cumulated vsize (Kb) 51056 [startup+980.084 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 97810 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 978.96 Current children cumulated vsize (Kb) 51056 [startup+990.085 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 98809 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 988.95 Current children cumulated vsize (Kb) 51056 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12063 0 2 0 99810 84 0 0 25 0 1 0 1782998965 50106368 12052 4294967295 134512640 135094434 3221224432 3221223084 134557062 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12233 12052 145 145 0 12088 0 [pid=12310] vsize: 48932 Current children cumulated CPU time (s) 998.96 Current children cumulated vsize (Kb) 51056 [startup+1010.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 100807 85 0 0 25 0 1 0 1782998965 50708480 12199 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12380 12199 145 145 0 12235 0 [pid=12310] vsize: 49520 Current children cumulated CPU time (s) 1008.94 Current children cumulated vsize (Kb) 51644 [startup+1020.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 101808 85 0 0 25 0 1 0 1782998965 50708480 12199 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12380 12199 145 145 0 12235 0 [pid=12310] vsize: 49520 Current children cumulated CPU time (s) 1018.95 Current children cumulated vsize (Kb) 51644 [startup+1030.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 102808 85 0 0 25 0 1 0 1782998965 50708480 12199 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12380 12199 145 145 0 12235 0 [pid=12310] vsize: 49520 Current children cumulated CPU time (s) 1028.95 Current children cumulated vsize (Kb) 51644 [startup+1040.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 103808 85 0 0 25 0 1 0 1782998965 50708480 12199 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12380 12199 145 145 0 12235 0 [pid=12310] vsize: 49520 Current children cumulated CPU time (s) 1038.95 Current children cumulated vsize (Kb) 51644 [startup+1050.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 104808 85 0 0 25 0 1 0 1782998965 50708480 12199 4294967295 134512640 135094434 3221224432 3221223024 134557401 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12380 12199 145 145 0 12235 0 [pid=12310] vsize: 49520 Current children cumulated CPU time (s) 1048.95 Current children cumulated vsize (Kb) 51644 [startup+1060.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 105808 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223104 134556236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1058.95 Current children cumulated vsize (Kb) 51036 [startup+1070.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 106808 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1068.95 Current children cumulated vsize (Kb) 51036 [startup+1080.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 107809 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1078.96 Current children cumulated vsize (Kb) 51036 [startup+1090.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 108809 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1088.96 Current children cumulated vsize (Kb) 51036 [startup+1100.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 109809 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1098.96 Current children cumulated vsize (Kb) 51036 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 110809 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1108.96 Current children cumulated vsize (Kb) 51036 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12210 0 2 0 111809 85 0 0 25 0 1 0 1782998965 50085888 12047 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12228 12047 145 145 0 12083 0 [pid=12310] vsize: 48912 Current children cumulated CPU time (s) 1118.96 Current children cumulated vsize (Kb) 51036 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 112802 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1128.92 Current children cumulated vsize (Kb) 53096 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 113803 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223024 134557208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1138.93 Current children cumulated vsize (Kb) 53096 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 114803 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1148.93 Current children cumulated vsize (Kb) 53096 [startup+1160.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 115803 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1158.93 Current children cumulated vsize (Kb) 53096 [startup+1170.09 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 116803 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1168.93 Current children cumulated vsize (Kb) 53096 [startup+1180.1 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 12725 0 2 0 117803 88 0 0 25 0 1 0 1782998965 52195328 12562 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 12743 12562 145 145 0 12598 0 [pid=12310] vsize: 50972 Current children cumulated CPU time (s) 1178.93 Current children cumulated vsize (Kb) 53096 [startup+1190.1 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 13045 0 2 0 118798 91 0 0 25 0 1 0 1782998965 53514240 12882 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 13065 12882 145 145 0 12920 0 [pid=12310] vsize: 52260 Current children cumulated CPU time (s) 1188.91 Current children cumulated vsize (Kb) 54384 [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 13438 0 2 0 119791 94 0 0 25 0 1 0 1782998965 55152640 13275 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 13465 13275 145 145 0 13320 0 [pid=12310] vsize: 53860 Current children cumulated CPU time (s) 1198.87 Current children cumulated vsize (Kb) 55984 [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 13491 0 2 0 120790 94 0 0 25 0 1 0 1782998965 55369728 13328 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 13518 13328 145 145 0 13373 0 [pid=12310] vsize: 54072 Current children cumulated CPU time (s) 1208.86 Current children cumulated vsize (Kb) 56196 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.91 2/57 12310 Raw data (/proc/12306/stat): 12306 (minisat+_script) S 12305 12306 9854 0 -1 0 288 236 1 3 0 1 0 1 20 0 1 0 1782998956 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/12306/statm): 531 226 485 147 0 384 0 [pid=12306] vsize: 2124 Raw data (/proc/12310/stat): 12310 (minisat+_64-bit) R 12306 12306 9854 0 -1 0 13491 0 2 0 120790 94 0 0 25 0 1 0 1782998965 55369728 13328 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/12310/statm): 13518 13328 145 145 0 13373 0 [pid=12310] vsize: 54072 Current children cumulated CPU time (s) 1208.86 Current children cumulated vsize (Kb) 56196 Sending SIGTERM to -12306 Sleeping 2 seconds One traced child (pid=12306) ended because it received signal 15 (SIGTERM) One traced child (pid=12310) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.13 CPU time (s): 1208.88 CPU user time (s): 1207.91 CPU system time (s): 0.973851 CPU usage (%): 99.8972 Max. virtual memory (cumulated for all children) (Kb): 56196
ERROR: no interpretation found !