Name | submitted/manquinho/primes-dimacs-cnf/normalized-ii8b1.opb |
MD5SUM | 812314147c77e28d5e428080c7a2412d |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 191 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 672 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 672 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 672 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.08 |
Number of variables | 672 |
Total number of constraints | 2404 |
Number of constraints which are clauses | 2404 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 8 |
LAUNCH ON wulflinc24 THE 2005-09-18 15:23:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2502 boxname=wulflinc24 idbench=158 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 812314147c77e28d5e428080c7a2412d /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb IDLAUNCH: 2502 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 920780 kB Buffers: 34648 kB Cached: 51716 kB SwapCached: 744 kB Active: 62300 kB Inactive: 26704 kB HighTotal: 131008 kB HighFree: 76048 kB LowTotal: 903652 kB LowFree: 844732 kB SwapTotal: 2097892 kB SwapFree: 2096644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 19256 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 15:43:51 (client local time) WITH STATUS 10 IN 1209.61 SECONDS stats: 2502 7 1209.61 10
c Parsing PB file... c Converting 2404 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 2404 5328 | 801 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 224[0m c ---[ 0]---> Sorter-cost:30564 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 39371 91691 | 13123 2 14 7.0 | 0.000 % | c | 102 | 39094 91112 | 14435 93 3903 42.0 | 0.670 % | c | 252 | 39002 90914 | 15878 240 6701 27.9 | 0.882 % | c | 477 | 38987 90884 | 17466 464 15942 34.4 | 0.910 % | c | 815 | 37805 88284 | 19213 776 24356 31.4 | 3.726 % | c | 1322 | 37260 87073 | 21134 1269 45788 36.1 | 5.055 % | c | 2082 | 37129 86792 | 23248 2027 71701 35.4 | 5.354 % | c | 3223 | 37060 86641 | 25573 3166 105927 33.5 | 5.514 % | c | 4933 | 36659 85752 | 28130 4825 171835 35.6 | 6.479 % | c ============================================================================== c [1mFound solution: 213[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5130 | 36761 86021 | 12253 5022 174707 34.8 | 6.479 % | c | 5230 | 36692 85868 | 13478 5120 176718 34.5 | 6.749 % | c | 5381 | 36692 85868 | 14826 5271 182366 34.6 | 6.749 % | c | 5606 | 36692 85868 | 16308 5496 187885 34.2 | 6.749 % | c | 5944 | 36590 85644 | 17939 5831 206859 35.5 | 6.987 % | c | 6450 | 36554 85568 | 19733 6324 229508 36.3 | 7.063 % | c | 7209 | 36479 85399 | 21706 7081 256581 36.2 | 7.249 % | c | 8348 | 36479 85399 | 23877 8220 321429 39.1 | 7.249 % | c ============================================================================== c [1mFound solution: 212[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8492 | 36455 85340 | 12151 8328 322244 38.7 | 7.249 % | c | 8592 | 36412 85243 | 13366 8427 325487 38.6 | 7.439 % | c | 8742 | 36412 85243 | 14702 8577 331063 38.6 | 7.440 % | c ============================================================================== c [1mFound solution: 191[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8825 | 36570 85630 | 12190 8660 333479 38.5 | 7.440 % | c | 8925 | 36570 85630 | 13409 8760 336090 38.4 | 7.604 % | c | 9075 | 36570 85630 | 14749 8910 343099 38.5 | 7.604 % | c | 9301 | 36570 85630 | 16224 9136 351679 38.5 | 7.605 % | c | 9638 | 36570 85630 | 17847 9473 362266 38.2 | 7.604 % | c | 10144 | 36472 85414 | 19632 9977 379563 38.0 | 7.834 % | c | 10905 | 36472 85414 | 21595 10738 407634 38.0 | 7.834 % | c | 12044 | 36472 85414 | 23754 11877 468101 39.4 | 7.834 % | c | 13754 | 36472 85414 | 26130 13587 522596 38.5 | 7.834 % | c | 16317 | 36470 85410 | 28743 16149 629422 39.0 | 7.838 % | c | 20161 | 36426 85316 | 31617 19992 838045 41.9 | 7.936 % | c | 25927 | 36382 85218 | 34779 25757 1118768 43.4 | 8.043 % | c | 34576 | 36305 85037 | 38257 34348 1535481 44.7 | 8.244 % | c | 47550 | 36181 84771 | 42083 21274 996051 46.8 | 8.517 % | c | 67011 | 36135 84671 | 46291 40732 1888951 46.4 | 8.624 % | c | 96203 | 36135 84671 | 50920 35083 1330080 37.9 | 8.624 % | c | 139993 | 36085 84561 | 56012 42013 1861233 44.3 | 8.742 % | c | 205677 | 36085 84561 | 61613 20830 839310 40.3 | 8.742 % | c | 304203 | 36085 84561 | 67775 23016 997862 43.4 | 8.742 % |
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/24493/stat): 24493 (minisat+_script) R 24492 24493 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1842308236 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24493/statm): 174 3 169 147 0 27 0 [pid=24493] 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=24494 New process pid=24495 New process pid=24496 execve syscall for /bin/sed executable One traced child (pid=24495) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=24496) exited with status: 0 One traced child (pid=24494) exited with status: 0 New process pid=24497 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-ii8b1.opb [startup+10.0032 s] Raw data (loadavg): 0.92 0.95 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2243 0 0 0 978 8 0 0 25 0 1 0 1842308241 9736192 2176 4294967295 134512640 135094434 3221224448 3221223136 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 2377 2176 145 145 0 2232 0 [pid=24497] vsize: 9508 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 11632 [startup+20.0039 s] Raw data (loadavg): 0.93 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2535 0 0 0 1973 10 0 0 25 0 1 0 1842308241 11481088 2468 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 2803 2468 145 145 0 2658 0 [pid=24497] vsize: 11212 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 13336 [startup+30.0056 s] Raw data (loadavg): 0.94 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 2796 0 0 0 2967 12 0 0 25 0 1 0 1842308241 12529664 2729 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 3059 2729 145 145 0 2914 0 [pid=24497] vsize: 12236 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 14360 [startup+40.0063 s] Raw data (loadavg): 0.95 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3032 0 0 0 3963 14 0 0 25 0 1 0 1842308241 13545472 2965 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 3307 2965 145 145 0 3162 0 [pid=24497] vsize: 13228 Current children cumulated CPU time (s) 39.79 Current children cumulated vsize (Kb) 15352 [startup+50.008 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3238 0 0 0 4959 16 0 0 25 0 1 0 1842308241 14376960 3171 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 3510 3171 145 145 0 3365 0 [pid=24497] vsize: 14040 Current children cumulated CPU time (s) 49.77 Current children cumulated vsize (Kb) 16164 [startup+60.0087 s] Raw data (loadavg): 0.96 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3440 0 0 0 5954 18 0 0 25 0 1 0 1842308241 15187968 3373 4294967295 134512640 135094434 3221224448 3221223104 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 3708 3373 145 145 0 3563 0 [pid=24497] vsize: 14832 Current children cumulated CPU time (s) 59.74 Current children cumulated vsize (Kb) 16956 [startup+70.0094 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3611 0 0 0 6950 19 0 0 25 0 1 0 1842308241 15876096 3544 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 3876 3544 145 145 0 3731 0 [pid=24497] vsize: 15504 Current children cumulated CPU time (s) 69.71 Current children cumulated vsize (Kb) 17628 [startup+80.0111 s] Raw data (loadavg): 0.97 0.96 0.98 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3768 0 0 0 7947 21 0 0 25 0 1 0 1842308241 16510976 3701 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4031 3701 145 145 0 3886 0 [pid=24497] vsize: 16124 Current children cumulated CPU time (s) 79.7 Current children cumulated vsize (Kb) 18248 [startup+90.0118 s] Raw data (loadavg): 1.05 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 3967 0 0 0 8944 22 0 0 25 0 1 0 1842308241 17457152 3900 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4262 3900 145 145 0 4117 0 [pid=24497] vsize: 17048 Current children cumulated CPU time (s) 89.68 Current children cumulated vsize (Kb) 19172 [startup+100.013 s] Raw data (loadavg): 1.04 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4163 0 0 0 9940 23 0 0 25 0 1 0 1842308241 18259968 4096 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4458 4096 145 145 0 4313 0 [pid=24497] vsize: 17832 Current children cumulated CPU time (s) 99.65 Current children cumulated vsize (Kb) 19956 [startup+110.013 s] Raw data (loadavg): 1.04 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4381 0 0 0 10936 25 0 0 25 0 1 0 1842308241 19144704 4314 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4674 4314 145 145 0 4529 0 [pid=24497] vsize: 18696 Current children cumulated CPU time (s) 109.63 Current children cumulated vsize (Kb) 20820 [startup+120.014 s] Raw data (loadavg): 1.03 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4503 0 0 0 11933 26 0 0 25 0 1 0 1842308241 19636224 4436 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4794 4436 145 145 0 4649 0 [pid=24497] vsize: 19176 Current children cumulated CPU time (s) 119.61 Current children cumulated vsize (Kb) 21300 [startup+130.015 s] Raw data (loadavg): 1.02 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4508 0 0 0 12934 26 0 0 25 0 1 0 1842308241 19668992 4441 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4802 4441 145 145 0 4657 0 [pid=24497] vsize: 19208 Current children cumulated CPU time (s) 129.62 Current children cumulated vsize (Kb) 21332 [startup+140.015 s] Raw data (loadavg): 1.02 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4509 0 0 0 13934 26 0 0 25 0 1 0 1842308241 19668992 4442 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4802 4442 145 145 0 4657 0 [pid=24497] vsize: 19208 Current children cumulated CPU time (s) 139.62 Current children cumulated vsize (Kb) 21332 [startup+150.016 s] Raw data (loadavg): 1.02 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4513 0 0 0 14934 26 0 0 25 0 1 0 1842308241 19685376 4446 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4806 4446 145 145 0 4661 0 [pid=24497] vsize: 19224 Current children cumulated CPU time (s) 149.62 Current children cumulated vsize (Kb) 21348 [startup+160.017 s] Raw data (loadavg): 1.01 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4516 0 0 0 15934 27 0 0 25 0 1 0 1842308241 19718144 4449 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4814 4449 145 145 0 4669 0 [pid=24497] vsize: 19256 Current children cumulated CPU time (s) 159.63 Current children cumulated vsize (Kb) 21380 [startup+170.017 s] Raw data (loadavg): 1.01 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4528 0 0 0 16934 27 0 0 25 0 1 0 1842308241 19767296 4461 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4826 4461 145 145 0 4681 0 [pid=24497] vsize: 19304 Current children cumulated CPU time (s) 169.63 Current children cumulated vsize (Kb) 21428 [startup+180.018 s] Raw data (loadavg): 1.01 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4530 0 0 0 17934 27 0 0 25 0 1 0 1842308241 19767296 4463 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4826 4463 145 145 0 4681 0 [pid=24497] vsize: 19304 Current children cumulated CPU time (s) 179.63 Current children cumulated vsize (Kb) 21428 [startup+190.019 s] Raw data (loadavg): 1.01 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4571 0 0 0 18933 27 0 0 25 0 1 0 1842308241 19939328 4504 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 4868 4504 145 145 0 4723 0 [pid=24497] vsize: 19472 Current children cumulated CPU time (s) 189.62 Current children cumulated vsize (Kb) 21596 [startup+200.02 s] Raw data (loadavg): 1.01 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4708 0 0 0 19931 28 0 0 25 0 1 0 1842308241 20492288 4641 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5003 4641 145 145 0 4858 0 [pid=24497] vsize: 20012 Current children cumulated CPU time (s) 199.61 Current children cumulated vsize (Kb) 22136 [startup+210.021 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4833 0 0 0 20928 29 0 0 25 0 1 0 1842308241 21000192 4766 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5127 4766 145 145 0 4982 0 [pid=24497] vsize: 20508 Current children cumulated CPU time (s) 209.59 Current children cumulated vsize (Kb) 22632 [startup+220.022 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 4968 0 0 0 21926 30 0 0 25 0 1 0 1842308241 21544960 4901 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5260 4901 145 145 0 5115 0 [pid=24497] vsize: 21040 Current children cumulated CPU time (s) 219.58 Current children cumulated vsize (Kb) 23164 [startup+230.024 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5106 0 0 0 22924 31 0 0 25 0 1 0 1842308241 22097920 5039 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5395 5039 145 145 0 5250 0 [pid=24497] vsize: 21580 Current children cumulated CPU time (s) 229.57 Current children cumulated vsize (Kb) 23704 [startup+240.023 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5114 0 0 0 23924 31 0 0 25 0 1 0 1842308241 22130688 5047 4294967295 134512640 135094434 3221224448 3221223088 134562041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5403 5047 145 145 0 5258 0 [pid=24497] vsize: 21612 Current children cumulated CPU time (s) 239.57 Current children cumulated vsize (Kb) 23736 [startup+250.024 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5117 0 0 0 24924 31 0 0 25 0 1 0 1842308241 22196224 5050 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5419 5050 145 145 0 5274 0 [pid=24497] vsize: 21676 Current children cumulated CPU time (s) 249.57 Current children cumulated vsize (Kb) 23800 [startup+260.025 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5123 0 0 0 25924 31 0 0 25 0 1 0 1842308241 22196224 5056 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5419 5056 145 145 0 5274 0 [pid=24497] vsize: 21676 Current children cumulated CPU time (s) 259.57 Current children cumulated vsize (Kb) 23800 [startup+270.025 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5129 0 0 0 26925 31 0 0 25 0 1 0 1842308241 22228992 5062 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5427 5062 145 145 0 5282 0 [pid=24497] vsize: 21708 Current children cumulated CPU time (s) 269.58 Current children cumulated vsize (Kb) 23832 [startup+280.026 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5141 0 0 0 27925 31 0 0 25 0 1 0 1842308241 22294528 5074 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5443 5074 145 145 0 5298 0 [pid=24497] vsize: 21772 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 23896 [startup+290.027 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5143 0 0 0 28925 31 0 0 25 0 1 0 1842308241 22294528 5076 4294967295 134512640 135094434 3221224448 3221223104 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5443 5076 145 145 0 5298 0 [pid=24497] vsize: 21772 Current children cumulated CPU time (s) 289.58 Current children cumulated vsize (Kb) 23896 [startup+300.027 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5155 0 0 0 29925 31 0 0 25 0 1 0 1842308241 22392832 5088 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5467 5088 145 145 0 5322 0 [pid=24497] vsize: 21868 Current children cumulated CPU time (s) 299.58 Current children cumulated vsize (Kb) 23992 [startup+310.028 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5169 0 0 0 30925 31 0 0 25 0 1 0 1842308241 22458368 5102 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5483 5102 145 145 0 5338 0 [pid=24497] vsize: 21932 Current children cumulated CPU time (s) 309.58 Current children cumulated vsize (Kb) 24056 [startup+320.029 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5171 0 0 0 31926 31 0 0 25 0 1 0 1842308241 22458368 5104 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5483 5104 145 145 0 5338 0 [pid=24497] vsize: 21932 Current children cumulated CPU time (s) 319.59 Current children cumulated vsize (Kb) 24056 [startup+330.03 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5183 0 0 0 32926 31 0 0 25 0 1 0 1842308241 22523904 5116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5499 5116 145 145 0 5354 0 [pid=24497] vsize: 21996 Current children cumulated CPU time (s) 329.59 Current children cumulated vsize (Kb) 24120 [startup+340.03 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5186 0 0 0 33926 31 0 0 25 0 1 0 1842308241 22523904 5119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5499 5119 145 145 0 5354 0 [pid=24497] vsize: 21996 Current children cumulated CPU time (s) 339.59 Current children cumulated vsize (Kb) 24120 [startup+350.032 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5205 0 0 0 34926 31 0 0 25 0 1 0 1842308241 22654976 5138 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5531 5138 145 145 0 5386 0 [pid=24497] vsize: 22124 Current children cumulated CPU time (s) 349.59 Current children cumulated vsize (Kb) 24248 [startup+360.033 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5209 0 0 0 35927 31 0 0 25 0 1 0 1842308241 22654976 5142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5531 5142 145 145 0 5386 0 [pid=24497] vsize: 22124 Current children cumulated CPU time (s) 359.6 Current children cumulated vsize (Kb) 24248 [startup+370.032 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 36926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0 [pid=24497] vsize: 22352 Current children cumulated CPU time (s) 369.59 Current children cumulated vsize (Kb) 24476 [startup+380.033 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 37926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134556999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0 [pid=24497] vsize: 22352 Current children cumulated CPU time (s) 379.59 Current children cumulated vsize (Kb) 24476 [startup+390.034 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 38926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223040 134557423 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0 [pid=24497] vsize: 22352 Current children cumulated CPU time (s) 389.59 Current children cumulated vsize (Kb) 24476 [startup+400.034 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5267 0 0 0 39926 31 0 0 25 0 1 0 1842308241 22888448 5200 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5588 5200 145 145 0 5443 0 [pid=24497] vsize: 22352 Current children cumulated CPU time (s) 399.59 Current children cumulated vsize (Kb) 24476 [startup+410.035 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5271 0 0 0 40926 31 0 0 25 0 1 0 1842308241 22904832 5204 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5592 5204 145 145 0 5447 0 [pid=24497] vsize: 22368 Current children cumulated CPU time (s) 409.59 Current children cumulated vsize (Kb) 24492 [startup+420.036 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 41927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0 [pid=24497] vsize: 22400 Current children cumulated CPU time (s) 419.6 Current children cumulated vsize (Kb) 24524 [startup+430.036 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 42927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0 [pid=24497] vsize: 22400 Current children cumulated CPU time (s) 429.6 Current children cumulated vsize (Kb) 24524 [startup+440.037 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5277 0 0 0 43927 31 0 0 25 0 1 0 1842308241 22937600 5210 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5600 5210 145 145 0 5455 0 [pid=24497] vsize: 22400 Current children cumulated CPU time (s) 439.6 Current children cumulated vsize (Kb) 24524 [startup+450.038 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5292 0 0 0 44927 31 0 0 25 0 1 0 1842308241 23003136 5225 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5616 5225 145 145 0 5471 0 [pid=24497] vsize: 22464 Current children cumulated CPU time (s) 449.6 Current children cumulated vsize (Kb) 24588 [startup+460.039 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5300 0 0 0 45927 32 0 0 25 0 1 0 1842308241 23035904 5233 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5624 5233 145 145 0 5479 0 [pid=24497] vsize: 22496 Current children cumulated CPU time (s) 459.61 Current children cumulated vsize (Kb) 24620 [startup+470.039 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5301 0 0 0 46927 32 0 0 25 0 1 0 1842308241 23035904 5234 4294967295 134512640 135094434 3221224448 3221223040 134557393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5624 5234 145 145 0 5479 0 [pid=24497] vsize: 22496 Current children cumulated CPU time (s) 469.61 Current children cumulated vsize (Kb) 24620 [startup+480.04 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5319 0 0 0 47927 32 0 0 25 0 1 0 1842308241 23134208 5252 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5648 5252 145 145 0 5503 0 [pid=24497] vsize: 22592 Current children cumulated CPU time (s) 479.61 Current children cumulated vsize (Kb) 24716 [startup+490.041 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5326 0 0 0 48928 32 0 0 25 0 1 0 1842308241 23232512 5259 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5672 5259 145 145 0 5527 0 [pid=24497] vsize: 22688 Current children cumulated CPU time (s) 489.62 Current children cumulated vsize (Kb) 24812 [startup+500.042 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5474 0 0 0 49924 33 0 0 25 0 1 0 1842308241 23777280 5407 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5805 5407 145 145 0 5660 0 [pid=24497] vsize: 23220 Current children cumulated CPU time (s) 499.59 Current children cumulated vsize (Kb) 25344 [startup+510.043 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5607 0 0 0 50921 35 0 0 25 0 1 0 1842308241 24317952 5540 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 5937 5540 145 145 0 5792 0 [pid=24497] vsize: 23748 Current children cumulated CPU time (s) 509.58 Current children cumulated vsize (Kb) 25872 [startup+520.044 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5708 0 0 0 51919 36 0 0 25 0 1 0 1842308241 24719360 5641 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6035 5641 145 145 0 5890 0 [pid=24497] vsize: 24140 Current children cumulated CPU time (s) 519.57 Current children cumulated vsize (Kb) 26264 [startup+530.045 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 52918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 529.57 Current children cumulated vsize (Kb) 26696 [startup+540.046 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 53918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 539.57 Current children cumulated vsize (Kb) 26696 [startup+550.047 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 54918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 549.57 Current children cumulated vsize (Kb) 26696 [startup+560.048 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 55918 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223104 134558147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 559.57 Current children cumulated vsize (Kb) 26696 [startup+570.048 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5819 0 0 0 56919 37 0 0 25 0 1 0 1842308241 25161728 5752 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5752 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 569.58 Current children cumulated vsize (Kb) 26696 [startup+580.049 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5820 0 0 0 57919 37 0 0 25 0 1 0 1842308241 25161728 5753 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5753 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 579.58 Current children cumulated vsize (Kb) 26696 [startup+590.05 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5820 0 0 0 58919 37 0 0 25 0 1 0 1842308241 25161728 5753 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6143 5753 145 145 0 5998 0 [pid=24497] vsize: 24572 Current children cumulated CPU time (s) 589.58 Current children cumulated vsize (Kb) 26696 [startup+600.051 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5855 0 0 0 59919 37 0 0 25 0 1 0 1842308241 25358336 5788 4294967295 134512640 135094434 3221224448 3221223072 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6191 5788 145 145 0 6046 0 [pid=24497] vsize: 24764 Current children cumulated CPU time (s) 599.58 Current children cumulated vsize (Kb) 26888 [startup+610.052 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5855 0 0 0 60919 37 0 0 25 0 1 0 1842308241 25358336 5788 4294967295 134512640 135094434 3221224448 3221223040 134556806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6191 5788 145 145 0 6046 0 [pid=24497] vsize: 24764 Current children cumulated CPU time (s) 609.58 Current children cumulated vsize (Kb) 26888 [startup+620.053 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5860 0 0 0 61919 37 0 0 25 0 1 0 1842308241 25489408 5793 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5793 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 619.58 Current children cumulated vsize (Kb) 27016 [startup+630.053 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5863 0 0 0 62920 37 0 0 25 0 1 0 1842308241 25489408 5796 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5796 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 629.59 Current children cumulated vsize (Kb) 27016 [startup+640.054 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5863 0 0 0 63920 37 0 0 25 0 1 0 1842308241 25489408 5796 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5796 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 639.59 Current children cumulated vsize (Kb) 27016 [startup+650.055 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5864 0 0 0 64920 37 0 0 25 0 1 0 1842308241 25489408 5797 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5797 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 649.59 Current children cumulated vsize (Kb) 27016 [startup+660.056 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5864 0 0 0 65920 37 0 0 25 0 1 0 1842308241 25489408 5797 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5797 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 659.59 Current children cumulated vsize (Kb) 27016 [startup+670.056 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5865 0 0 0 66921 37 0 0 25 0 1 0 1842308241 25489408 5798 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5798 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 669.6 Current children cumulated vsize (Kb) 27016 [startup+680.057 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5869 0 0 0 67921 37 0 0 25 0 1 0 1842308241 25489408 5802 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6223 5802 145 145 0 6078 0 [pid=24497] vsize: 24892 Current children cumulated CPU time (s) 679.6 Current children cumulated vsize (Kb) 27016 [startup+690.058 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 5939 0 0 0 68920 37 0 0 25 0 1 0 1842308241 25714688 5872 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6278 5872 145 145 0 6133 0 [pid=24497] vsize: 25112 Current children cumulated CPU time (s) 689.59 Current children cumulated vsize (Kb) 27236 [startup+700.059 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 69919 38 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 699.59 Current children cumulated vsize (Kb) 27492 [startup+710.06 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 70919 38 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 709.59 Current children cumulated vsize (Kb) 27492 [startup+720.061 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6001 0 0 0 71918 39 0 0 25 0 1 0 1842308241 25976832 5934 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5934 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 719.59 Current children cumulated vsize (Kb) 27492 [startup+730.061 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 72918 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 729.59 Current children cumulated vsize (Kb) 27492 [startup+740.062 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 73919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 739.6 Current children cumulated vsize (Kb) 27492 [startup+750.063 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 74919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 749.6 Current children cumulated vsize (Kb) 27492 [startup+760.063 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 75919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 759.6 Current children cumulated vsize (Kb) 27492 [startup+770.064 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 76919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 769.6 Current children cumulated vsize (Kb) 27492 [startup+780.066 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 77919 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 779.6 Current children cumulated vsize (Kb) 27492 [startup+790.067 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 78920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 789.61 Current children cumulated vsize (Kb) 27492 [startup+800.067 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 79920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 799.61 Current children cumulated vsize (Kb) 27492 [startup+810.068 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 80920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 809.61 Current children cumulated vsize (Kb) 27492 [startup+820.069 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 81920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 819.61 Current children cumulated vsize (Kb) 27492 [startup+830.069 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 82920 39 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 829.61 Current children cumulated vsize (Kb) 27492 [startup+840.07 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 83920 40 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 839.62 Current children cumulated vsize (Kb) 27492 [startup+850.072 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6002 0 0 0 84921 40 0 0 25 0 1 0 1842308241 25976832 5935 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 6342 5935 145 145 0 6197 0 [pid=24497] vsize: 25368 Current children cumulated CPU time (s) 849.63 Current children cumulated vsize (Kb) 27492 [startup+860.072 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6152 0 0 0 85918 41 0 0 25 0 1 0 1842308241 26591232 6085 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6492 6085 145 145 0 6347 0 [pid=24497] vsize: 25968 Current children cumulated CPU time (s) 859.61 Current children cumulated vsize (Kb) 28092 [startup+870.073 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6303 0 0 0 86915 42 0 0 25 0 1 0 1842308241 27209728 6236 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6643 6236 145 145 0 6498 0 [pid=24497] vsize: 26572 Current children cumulated CPU time (s) 869.59 Current children cumulated vsize (Kb) 28696 [startup+880.075 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 87912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223040 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0 [pid=24497] vsize: 27388 Current children cumulated CPU time (s) 879.58 Current children cumulated vsize (Kb) 29512 [startup+890.076 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 88912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0 [pid=24497] vsize: 27388 Current children cumulated CPU time (s) 889.58 Current children cumulated vsize (Kb) 29512 [startup+900.077 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6444 0 0 0 89912 44 0 0 25 0 1 0 1842308241 28045312 6377 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6847 6377 145 145 0 6702 0 [pid=24497] vsize: 27388 Current children cumulated CPU time (s) 899.58 Current children cumulated vsize (Kb) 29512 [startup+910.079 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6445 0 0 0 90911 45 0 0 25 0 1 0 1842308241 28045312 6378 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6847 6378 145 145 0 6702 0 [pid=24497] vsize: 27388 Current children cumulated CPU time (s) 909.58 Current children cumulated vsize (Kb) 29512 [startup+920.08 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6447 0 0 0 91911 45 0 0 25 0 1 0 1842308241 28057600 6380 4294967295 134512640 135094434 3221224448 3221223104 134558279 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6850 6380 145 145 0 6705 0 [pid=24497] vsize: 27400 Current children cumulated CPU time (s) 919.58 Current children cumulated vsize (Kb) 29524 [startup+930.081 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6447 0 0 0 92911 46 0 0 25 0 1 0 1842308241 28057600 6380 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6850 6380 145 145 0 6705 0 [pid=24497] vsize: 27400 Current children cumulated CPU time (s) 929.59 Current children cumulated vsize (Kb) 29524 [startup+940.082 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6459 0 0 0 93910 46 0 0 25 0 1 0 1842308241 28106752 6392 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6862 6392 145 145 0 6717 0 [pid=24497] vsize: 27448 Current children cumulated CPU time (s) 939.58 Current children cumulated vsize (Kb) 29572 [startup+950.084 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6466 0 0 0 94910 47 0 0 25 0 1 0 1842308241 28139520 6399 4294967295 134512640 135094434 3221224448 3221223120 134555576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6870 6399 145 145 0 6725 0 [pid=24497] vsize: 27480 Current children cumulated CPU time (s) 949.59 Current children cumulated vsize (Kb) 29604 [startup+960.085 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6478 0 0 0 95909 48 0 0 25 0 1 0 1842308241 28188672 6411 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6882 6411 145 145 0 6737 0 [pid=24497] vsize: 27528 Current children cumulated CPU time (s) 959.59 Current children cumulated vsize (Kb) 29652 [startup+970.085 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6490 0 0 0 96909 48 0 0 25 0 1 0 1842308241 28286976 6423 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6906 6423 145 145 0 6761 0 [pid=24497] vsize: 27624 Current children cumulated CPU time (s) 969.59 Current children cumulated vsize (Kb) 29748 [startup+980.087 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6495 0 0 0 97909 48 0 0 25 0 1 0 1842308241 28286976 6428 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6906 6428 145 145 0 6761 0 [pid=24497] vsize: 27624 Current children cumulated CPU time (s) 979.59 Current children cumulated vsize (Kb) 29748 [startup+990.089 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6497 0 0 0 98909 49 0 0 25 0 1 0 1842308241 28286976 6430 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6906 6430 145 145 0 6761 0 [pid=24497] vsize: 27624 Current children cumulated CPU time (s) 989.6 Current children cumulated vsize (Kb) 29748 [startup+1000.09 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6514 0 0 0 99908 49 0 0 25 0 1 0 1842308241 28352512 6447 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6922 6447 145 145 0 6777 0 [pid=24497] vsize: 27688 Current children cumulated CPU time (s) 999.59 Current children cumulated vsize (Kb) 29812 [startup+1010.09 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6530 0 0 0 100907 50 0 0 25 0 1 0 1842308241 28418048 6463 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6938 6463 145 145 0 6793 0 [pid=24497] vsize: 27752 Current children cumulated CPU time (s) 1009.59 Current children cumulated vsize (Kb) 29876 [startup+1020.09 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6532 0 0 0 101906 51 0 0 25 0 1 0 1842308241 28418048 6465 4294967295 134512640 135094434 3221224448 3221223040 134557271 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6938 6465 145 145 0 6793 0 [pid=24497] vsize: 27752 Current children cumulated CPU time (s) 1019.59 Current children cumulated vsize (Kb) 29876 [startup+1030.09 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6551 0 0 0 102904 53 0 0 25 0 1 0 1842308241 28614656 6484 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6986 6484 145 145 0 6841 0 [pid=24497] vsize: 27944 Current children cumulated CPU time (s) 1029.59 Current children cumulated vsize (Kb) 30068 [startup+1040.09 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6557 0 0 0 103903 54 0 0 25 0 1 0 1842308241 28614656 6490 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 6986 6490 145 145 0 6841 0 [pid=24497] vsize: 27944 Current children cumulated CPU time (s) 1039.59 Current children cumulated vsize (Kb) 30068 [startup+1050.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6605 0 0 0 104902 55 0 0 25 0 1 0 1842308241 28749824 6538 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 7019 6538 145 145 0 6874 0 [pid=24497] vsize: 28076 Current children cumulated CPU time (s) 1049.59 Current children cumulated vsize (Kb) 30200 [startup+1060.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6742 0 0 0 105898 57 0 0 25 0 1 0 1842308241 29306880 6675 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 7155 6675 145 145 0 7010 0 [pid=24497] vsize: 28620 Current children cumulated CPU time (s) 1059.57 Current children cumulated vsize (Kb) 30744 [startup+1070.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 106897 58 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1069.57 Current children cumulated vsize (Kb) 30896 [startup+1080.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 107897 59 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1079.58 Current children cumulated vsize (Kb) 30896 [startup+1090.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 108896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1089.58 Current children cumulated vsize (Kb) 30896 [startup+1100.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 109896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1099.58 Current children cumulated vsize (Kb) 30896 [startup+1110.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 110896 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1109.58 Current children cumulated vsize (Kb) 30896 [startup+1120.1 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 111897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1119.59 Current children cumulated vsize (Kb) 30896 [startup+1130.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 112897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1129.59 Current children cumulated vsize (Kb) 30896 [startup+1140.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 113897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1139.59 Current children cumulated vsize (Kb) 30896 [startup+1150.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6784 0 0 0 114897 60 0 0 25 0 1 0 1842308241 29462528 6717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7193 6717 145 145 0 7048 0 [pid=24497] vsize: 28772 Current children cumulated CPU time (s) 1149.59 Current children cumulated vsize (Kb) 30896 [startup+1160.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6787 0 0 0 115897 60 0 0 25 0 1 0 1842308241 29478912 6720 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7197 6720 145 145 0 7052 0 [pid=24497] vsize: 28788 Current children cumulated CPU time (s) 1159.59 Current children cumulated vsize (Kb) 30912 [startup+1170.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6790 0 0 0 116898 60 0 0 25 0 1 0 1842308241 29495296 6723 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7201 6723 145 145 0 7056 0 [pid=24497] vsize: 28804 Current children cumulated CPU time (s) 1169.6 Current children cumulated vsize (Kb) 30928 [startup+1180.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 117898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0 [pid=24497] vsize: 28836 Current children cumulated CPU time (s) 1179.6 Current children cumulated vsize (Kb) 30960 [startup+1190.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 118898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0 [pid=24497] vsize: 28836 Current children cumulated CPU time (s) 1189.6 Current children cumulated vsize (Kb) 30960 [startup+1200.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6797 0 0 0 119898 60 0 0 25 0 1 0 1842308241 29528064 6730 4294967295 134512640 135094434 3221224448 3221223040 134557221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7209 6730 145 145 0 7064 0 [pid=24497] vsize: 28836 Current children cumulated CPU time (s) 1199.6 Current children cumulated vsize (Kb) 30960 [startup+1210.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6831 0 0 0 120898 60 0 0 25 0 1 0 1842308241 29691904 6764 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7249 6764 145 145 0 7104 0 [pid=24497] vsize: 28996 Current children cumulated CPU time (s) 1209.6 Current children cumulated vsize (Kb) 31120 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 1.00 0.98 0.99 2/57 24497 Raw data (/proc/24493/stat): 24493 (minisat+_script) S 24492 24493 20728 0 -1 0 288 239 0 0 0 1 0 1 22 0 1 0 1842308236 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24493/statm): 531 226 485 147 0 384 0 [pid=24493] vsize: 2124 Raw data (/proc/24497/stat): 24497 (minisat+_64-bit) R 24493 24493 20728 0 -1 0 6831 0 0 0 120898 60 0 0 25 0 1 0 1842308241 29691904 6764 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24497/statm): 7249 6764 145 145 0 7104 0 [pid=24497] vsize: 28996 Current children cumulated CPU time (s) 1209.6 Current children cumulated vsize (Kb) 31120 Sending SIGTERM to -24493 Sleeping 2 seconds One traced child (pid=24493) ended because it received signal 15 (SIGTERM) One traced child (pid=24497) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.13 CPU time (s): 1209.61 CPU user time (s): 1208.99 CPU system time (s): 0.622905 CPU usage (%): 99.9571 Max. virtual memory (cumulated for all children) (Kb): 31120
ERROR: no interpretation found !