Name | submitted/sorensson/garden/normalized-g15x15.opb |
MD5SUM | 6a083b86cc55025d2acb3bcf68562064 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 54 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 225 |
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 | 225 |
Number of bits of the sum of numbers in the objective function | 8 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 225 |
Number of bits of the biggest sum of numbers | 8 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.11 |
Number of variables | 225 |
Total number of constraints | 225 |
Number of constraints which are clauses | 225 |
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 | 3 |
Maximum length of a constraint | 5 |
LAUNCH ON wulflinc28 THE 2005-09-18 18:13:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2611 boxname=wulflinc28 idbench=267 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6a083b86cc55025d2acb3bcf68562064 /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb IDLAUNCH: 2611 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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: 931140 kB Buffers: 33860 kB Cached: 41672 kB SwapCached: 696 kB Active: 60744 kB Inactive: 17248 kB HighTotal: 131008 kB HighFree: 85792 kB LowTotal: 903652 kB LowFree: 845348 kB SwapTotal: 2097640 kB SwapFree: 2096372 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5812 kB Slab: 19848 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:34:09 (client local time) WITH STATUS 10 IN 1209.89 SECONDS stats: 2611 7 1209.89 10
c Parsing PB file... c Converting 225 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 | 225 1065 | 75 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 75[0m c ---[ 0]---> Sorter-cost: 6660 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 7880 18944 | 2626 0 0 nan | 0.000 % | c | 101 | 7833 18849 | 2888 96 1463 15.2 | 0.648 % | c | 251 | 7833 18849 | 3177 246 4130 16.8 | 0.648 % | c | 476 | 7833 18849 | 3495 471 7548 16.0 | 0.648 % | c | 813 | 7815 18811 | 3844 807 14594 18.1 | 0.839 % | c | 1319 | 7815 18811 | 4229 1313 22407 17.1 | 0.839 % | c | 2078 | 7815 18811 | 4652 2072 35096 16.9 | 0.839 % | c | 3218 | 7778 18732 | 5117 3196 64657 20.2 | 1.240 % | c ============================================================================== c [1mFound solution: 62[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3831 | 7874 18967 | 2624 3809 80986 21.3 | 1.240 % | c | 3932 | 7874 18967 | 2886 2006 47019 23.4 | 1.244 % | c | 4083 | 7858 18933 | 3175 2156 49776 23.1 | 1.414 % | c | 4311 | 7842 18899 | 3492 2383 52246 21.9 | 1.583 % | c | 4648 | 7829 18870 | 3841 2710 55952 20.6 | 1.734 % | c | 5154 | 7800 18807 | 4225 2997 63106 21.1 | 2.055 % | c | 5913 | 7800 18807 | 4648 3756 76082 20.3 | 2.055 % | c | 7052 | 7800 18807 | 5113 4895 95383 19.5 | 2.055 % | c | 8760 | 7777 18758 | 5624 6599 132092 20.0 | 2.300 % | c | 11322 | 7777 18758 | 6187 5862 151993 25.9 | 2.300 % | c | 15166 | 7770 18743 | 6805 6264 166593 26.6 | 2.375 % | c | 20934 | 7746 18691 | 7486 4979 73086 14.7 | 2.639 % | c | 29584 | 7746 18691 | 8235 5495 121003 22.0 | 2.639 % | c | 42562 | 7746 18691 | 9058 8643 253958 29.4 | 2.639 % | c | 62023 | 7729 18654 | 9964 7482 293519 39.2 | 2.828 % | c ============================================================================== c [1mFound solution: 60[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82926 | 7732 18673 | 2577 5889 267788 45.5 | 2.828 % | c | 83026 | 7732 18673 | 2834 1573 37271 23.7 | 3.009 % | c | 83176 | 7732 18673 | 3118 1723 39197 22.7 | 3.009 % | c | 83401 | 7732 18673 | 3429 1948 43386 22.3 | 3.009 % | c | 83740 | 7732 18673 | 3772 2287 49778 21.8 | 3.009 % | c | 84246 | 7732 18673 | 4150 2793 58214 20.8 | 3.009 % | c | 85007 | 7730 18669 | 4565 3553 71012 20.0 | 3.028 % | c | 86147 | 7730 18669 | 5021 4693 101468 21.6 | 3.028 % | c | 87855 | 7730 18669 | 5524 3686 79696 21.6 | 3.028 % | c | 90417 | 7730 18669 | 6076 6248 143893 23.0 | 3.028 % | c | 94264 | 7730 18669 | 6684 6971 182901 26.2 | 3.028 % | c | 100033 | 7726 18661 | 7352 5471 139305 25.5 | 3.066 % | c | 108685 | 7726 18661 | 8087 6475 107535 16.6 | 3.066 % | c | 121659 | 7716 18639 | 8896 5512 193142 35.0 | 3.179 % | c | 141120 | 7716 18639 | 9786 9263 361472 39.0 | 3.178 % | c | 170312 | 7716 18639 | 10764 10279 353506 34.4 | 3.178 % | c | 214101 | 7716 18639 | 11841 11348 495137 43.6 | 3.178 % | c | 279785 | 7716 18639 | 13025 9072 248141 27.4 | 3.178 % | c | 378312 | 7716 18639 | 14327 7708 270624 35.1 | 3.178 % | c ============================================================================== c [1mFound solution: 58[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 518226 | 7738 18701 | 2579 14849 481198 32.4 | 3.178 % | c | 518326 | 7738 18701 | 2836 1957 43212 22.1 | 3.188 % | c | 518476 | 7738 18701 | 3120 2107 46360 22.0 | 3.188 % | c | 518703 | 7738 18701 | 3432 2334 50915 21.8 | 3.188 % | c | 519041 | 7738 18701 | 3775 2672 57879 21.7 | 3.188 % | c | 519549 | 7738 18701 | 4153 3180 67400 21.2 | 3.188 % | c | 520308 | 7738 18701 | 4568 3939 84338 21.4 | 3.188 % | c | 521447 | 7738 18701 | 5025 2631 43837 16.7 | 3.188 % | c | 523156 | 7713 18648 | 5528 2575 36654 14.2 | 3.451 % | c | 525720 | 7713 18648 | 6081 5139 109499 21.3 | 3.451 % | c | 529564 | 7713 18648 | 6689 8983 204736 22.8 | 3.451 % | c | 535331 | 7691 18600 | 7358 6698 147864 22.1 | 3.695 % | c | 543982 | 7691 18600 | 8094 6960 275619 39.6 | 3.695 % | c | 556956 | 7691 18600 | 8903 6646 246435 37.1 | 3.695 % | c | 576418 | 7691 18600 | 9793 10477 215457 20.6 | 3.695 % | c | 605612 | 7691 18600 | 10773 7116 272652 38.3 | 3.695 % | c | 649401 | 7678 18569 | 11850 10997 275428 25.0 | 3.863 % | c | 715085 | 7678 18569 | 13035 12319 413640 33.6 | 3.863 % | c | 813611 | 7678 18569 | 14339 7550 228042 30.2 | 3.863 % | c ============================================================================== c [1mFound solution: 56[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 851603 | 7695 18616 | 2565 12956 397284 30.7 | 3.863 % | c | 851703 | 7695 18616 | 2821 1720 31470 18.3 | 3.892 % | c | 851854 | 7695 18616 | 3103 1871 35434 18.9 | 3.892 % | c | 852081 | 7693 18612 | 3414 2097 38744 18.5 | 3.911 % | c | 852418 | 7693 18612 | 3755 2434 43532 17.9 | 3.911 % | c | 852924 | 7693 18612 | 4130 2940 56354 19.2 | 3.911 % | c | 853684 | 7693 18612 | 4544 3700 76355 20.6 | 3.911 % | c | 854827 | 7693 18612 | 4998 4843 102579 21.2 | 3.911 % | c | 856536 | 7693 18612 | 5498 3901 73991 19.0 | 3.911 % | c | 859099 | 7693 18612 | 6048 6464 145024 22.4 | 3.911 % | c | 862943 | 7690 18605 | 6652 3876 65509 16.9 | 3.948 % | c | 868714 | 7690 18605 | 7318 6158 115770 18.8 | 3.948 % | c | 877368 | 7690 18605 | 8050 7202 106459 14.8 | 3.948 % | c | 890342 | 7690 18605 | 8855 6654 235117 35.3 | 3.948 % | c | 909804 | 7680 18583 | 9740 7005 164322 23.5 | 4.061 % | c | 938996 | 7680 18583 | 10714 8504 305776 36.0 | 4.061 % | c | 982787 | 7680 18583 | 11786 11511 508585 44.2 | 4.061 % | c | 1048474 | 7680 18583 | 12964 11456 413707 36.1 | 4.061 % | c | 1147000 | 7678 18579 | 14261 12201 311601 25.5 | 4.079 % | c | 1294790 | 7661 18542 | 15687 15149 629931 41.6 | 4.266 % | c | 1516474 | 7658 18535 | 17256 16992 841342 49.5 | 4.304 % |
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/1972/stat): 1972 (minisat+_script) R 1971 1972 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843340199 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/1972/statm): 174 3 169 147 0 27 0 [pid=1972] 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=1973 New process pid=1974 New process pid=1975 execve syscall for /bin/sed executable One traced child (pid=1974) 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=1975) exited with status: 0 One traced child (pid=1973) exited with status: 0 New process pid=1976 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-g15x15.opb [startup+10.0048 s] Raw data (loadavg): 0.93 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 899 0 0 0 985 6 0 0 25 0 1 0 1843340204 4108288 885 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 1003 885 145 145 0 858 0 [pid=1976] vsize: 4012 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 6136 [startup+20.0065 s] Raw data (loadavg): 0.94 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1114 0 0 0 1981 7 0 0 25 0 1 0 1843340204 4980736 1100 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 1216 1100 145 145 0 1071 0 [pid=1976] vsize: 4864 Current children cumulated CPU time (s) 19.88 Current children cumulated vsize (Kb) 6988 [startup+30.0072 s] Raw data (loadavg): 0.95 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1298 0 0 0 2977 9 0 0 25 0 1 0 1843340204 5754880 1284 4294967295 134512640 135094434 3221224448 3221223100 134562194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 1405 1284 145 145 0 1260 0 [pid=1976] vsize: 5620 Current children cumulated CPU time (s) 29.86 Current children cumulated vsize (Kb) 7744 [startup+40.0078 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 3971 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0 [pid=1976] vsize: 6992 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 9116 [startup+50.0085 s] Raw data (loadavg): 0.96 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 4971 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0 [pid=1976] vsize: 6992 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 9116 [startup+60.0102 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 5972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0 [pid=1976] vsize: 6992 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 9116 [startup+70.0108 s] Raw data (loadavg): 0.97 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 6972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0 [pid=1976] vsize: 6992 Current children cumulated CPU time (s) 69.83 Current children cumulated vsize (Kb) 9116 [startup+80.0115 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1640 0 0 0 7972 11 0 0 25 0 1 0 1843340204 7159808 1626 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 1748 1626 145 145 0 1603 0 [pid=1976] vsize: 6992 Current children cumulated CPU time (s) 79.83 Current children cumulated vsize (Kb) 9116 [startup+90.0122 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1692 0 0 0 8972 12 0 0 25 0 1 0 1843340204 7368704 1678 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 1799 1678 145 145 0 1654 0 [pid=1976] vsize: 7196 Current children cumulated CPU time (s) 89.84 Current children cumulated vsize (Kb) 9320 [startup+100.012 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1936 0 0 0 9968 13 0 0 25 0 1 0 1843340204 8380416 1922 4294967295 134512640 135094434 3221224448 3221223060 134563046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2046 1922 145 145 0 1901 0 [pid=1976] vsize: 8184 Current children cumulated CPU time (s) 99.81 Current children cumulated vsize (Kb) 10308 [startup+110.014 s] Raw data (loadavg): 0.98 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1946 0 0 0 10968 13 0 0 25 0 1 0 1843340204 8437760 1932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2060 1932 145 145 0 1915 0 [pid=1976] vsize: 8240 Current children cumulated CPU time (s) 109.81 Current children cumulated vsize (Kb) 10364 [startup+120.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1946 0 0 0 11968 13 0 0 25 0 1 0 1843340204 8437760 1932 4294967295 134512640 135094434 3221224448 3221223088 134538540 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2060 1932 145 145 0 1915 0 [pid=1976] vsize: 8240 Current children cumulated CPU time (s) 119.81 Current children cumulated vsize (Kb) 10364 [startup+130.014 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1960 0 0 0 12969 13 0 0 25 0 1 0 1843340204 8503296 1946 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2076 1946 145 145 0 1931 0 [pid=1976] vsize: 8304 Current children cumulated CPU time (s) 129.82 Current children cumulated vsize (Kb) 10428 [startup+140.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1970 0 0 0 13969 13 0 0 25 0 1 0 1843340204 8552448 1956 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2088 1956 145 145 0 1943 0 [pid=1976] vsize: 8352 Current children cumulated CPU time (s) 139.82 Current children cumulated vsize (Kb) 10476 [startup+150.015 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 1999 0 0 0 14969 13 0 0 25 0 1 0 1843340204 8699904 1985 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2124 1985 145 145 0 1979 0 [pid=1976] vsize: 8496 Current children cumulated CPU time (s) 149.82 Current children cumulated vsize (Kb) 10620 [startup+160.016 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2009 0 0 0 15969 13 0 0 25 0 1 0 1843340204 8740864 1995 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2134 1995 145 145 0 1989 0 [pid=1976] vsize: 8536 Current children cumulated CPU time (s) 159.82 Current children cumulated vsize (Kb) 10660 [startup+170.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2015 0 0 0 16969 13 0 0 25 0 1 0 1843340204 8773632 2001 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2142 2001 145 145 0 1997 0 [pid=1976] vsize: 8568 Current children cumulated CPU time (s) 169.82 Current children cumulated vsize (Kb) 10692 [startup+180.017 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2074 0 0 0 17968 14 0 0 25 0 1 0 1843340204 9039872 2060 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2207 2060 145 145 0 2062 0 [pid=1976] vsize: 8828 Current children cumulated CPU time (s) 179.82 Current children cumulated vsize (Kb) 10952 [startup+190.018 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2167 0 0 0 18968 14 0 0 25 0 1 0 1843340204 9428992 2153 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2302 2153 145 145 0 2157 0 [pid=1976] vsize: 9208 Current children cumulated CPU time (s) 189.82 Current children cumulated vsize (Kb) 11332 [startup+200.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2180 0 0 0 19968 14 0 0 25 0 1 0 1843340204 9494528 2166 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2318 2166 145 145 0 2173 0 [pid=1976] vsize: 9272 Current children cumulated CPU time (s) 199.82 Current children cumulated vsize (Kb) 11396 [startup+210.019 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2180 0 0 0 20968 14 0 0 25 0 1 0 1843340204 9494528 2166 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2318 2166 145 145 0 2173 0 [pid=1976] vsize: 9272 Current children cumulated CPU time (s) 209.82 Current children cumulated vsize (Kb) 11396 [startup+220.02 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2188 0 0 0 21968 14 0 0 25 0 1 0 1843340204 9527296 2174 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2326 2174 145 145 0 2181 0 [pid=1976] vsize: 9304 Current children cumulated CPU time (s) 219.82 Current children cumulated vsize (Kb) 11428 [startup+230.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2194 0 0 0 22969 14 0 0 25 0 1 0 1843340204 9560064 2180 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2334 2180 145 145 0 2189 0 [pid=1976] vsize: 9336 Current children cumulated CPU time (s) 229.83 Current children cumulated vsize (Kb) 11460 [startup+240.021 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2234 0 0 0 23968 15 0 0 25 0 1 0 1843340204 9732096 2220 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2376 2220 145 145 0 2231 0 [pid=1976] vsize: 9504 Current children cumulated CPU time (s) 239.83 Current children cumulated vsize (Kb) 11628 [startup+250.022 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2246 0 0 0 24968 15 0 0 25 0 1 0 1843340204 9773056 2232 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2386 2232 145 145 0 2241 0 [pid=1976] vsize: 9544 Current children cumulated CPU time (s) 249.83 Current children cumulated vsize (Kb) 11668 [startup+260.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2320 0 0 0 25967 15 0 0 25 0 1 0 1843340204 10158080 2306 4294967295 134512640 135094434 3221224448 3221223104 134558286 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2480 2306 145 145 0 2335 0 [pid=1976] vsize: 9920 Current children cumulated CPU time (s) 259.82 Current children cumulated vsize (Kb) 12044 [startup+270.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2350 0 0 0 26968 15 0 0 25 0 1 0 1843340204 10276864 2336 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2509 2336 145 145 0 2364 0 [pid=1976] vsize: 10036 Current children cumulated CPU time (s) 269.83 Current children cumulated vsize (Kb) 12160 [startup+280.023 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2357 0 0 0 27968 15 0 0 25 0 1 0 1843340204 10301440 2343 4294967295 134512640 135094434 3221224448 3221223120 134556327 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2515 2343 145 145 0 2370 0 [pid=1976] vsize: 10060 Current children cumulated CPU time (s) 279.83 Current children cumulated vsize (Kb) 12184 [startup+290.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2389 0 0 0 28967 15 0 0 25 0 1 0 1843340204 10440704 2375 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2549 2375 145 145 0 2404 0 [pid=1976] vsize: 10196 Current children cumulated CPU time (s) 289.82 Current children cumulated vsize (Kb) 12320 [startup+300.024 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2402 0 0 0 29967 15 0 0 25 0 1 0 1843340204 10506240 2388 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2565 2388 145 145 0 2420 0 [pid=1976] vsize: 10260 Current children cumulated CPU time (s) 299.82 Current children cumulated vsize (Kb) 12384 [startup+310.025 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2407 0 0 0 30967 15 0 0 25 0 1 0 1843340204 10539008 2393 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2573 2393 145 145 0 2428 0 [pid=1976] vsize: 10292 Current children cumulated CPU time (s) 309.82 Current children cumulated vsize (Kb) 12416 [startup+320.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2419 0 0 0 31968 15 0 0 25 0 1 0 1843340204 10596352 2405 4294967295 134512640 135094434 3221224448 3221223040 134556884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2587 2405 145 145 0 2442 0 [pid=1976] vsize: 10348 Current children cumulated CPU time (s) 319.83 Current children cumulated vsize (Kb) 12472 [startup+330.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2451 0 0 0 32967 16 0 0 25 0 1 0 1843340204 10756096 2437 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2626 2437 145 145 0 2481 0 [pid=1976] vsize: 10504 Current children cumulated CPU time (s) 329.83 Current children cumulated vsize (Kb) 12628 [startup+340.026 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2474 0 0 0 33967 16 0 0 25 0 1 0 1843340204 10887168 2460 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2658 2460 145 145 0 2513 0 [pid=1976] vsize: 10632 Current children cumulated CPU time (s) 339.83 Current children cumulated vsize (Kb) 12756 [startup+350.027 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 34967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0 [pid=1976] vsize: 10648 Current children cumulated CPU time (s) 349.83 Current children cumulated vsize (Kb) 12772 [startup+360.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 35967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0 [pid=1976] vsize: 10648 Current children cumulated CPU time (s) 359.83 Current children cumulated vsize (Kb) 12772 [startup+370.029 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2480 0 0 0 36967 16 0 0 25 0 1 0 1843340204 10903552 2466 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2662 2466 145 145 0 2517 0 [pid=1976] vsize: 10648 Current children cumulated CPU time (s) 369.83 Current children cumulated vsize (Kb) 12772 [startup+380.03 s] Raw data (loadavg): 0.99 0.98 0.99 3/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2484 0 0 0 37967 16 0 0 25 0 1 0 1843340204 10919936 2470 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2666 2470 145 145 0 2521 0 [pid=1976] vsize: 10664 Current children cumulated CPU time (s) 379.83 Current children cumulated vsize (Kb) 12788 [startup+390.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2526 0 0 0 38967 16 0 0 25 0 1 0 1843340204 11100160 2512 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2710 2512 145 145 0 2565 0 [pid=1976] vsize: 10840 Current children cumulated CPU time (s) 389.83 Current children cumulated vsize (Kb) 12964 [startup+400.03 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2546 0 0 0 39967 17 0 0 25 0 1 0 1843340204 11182080 2532 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2730 2532 145 145 0 2585 0 [pid=1976] vsize: 10920 Current children cumulated CPU time (s) 399.84 Current children cumulated vsize (Kb) 13044 [startup+410.031 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2564 0 0 0 40967 17 0 0 25 0 1 0 1843340204 11264000 2550 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2750 2550 145 145 0 2605 0 [pid=1976] vsize: 11000 Current children cumulated CPU time (s) 409.84 Current children cumulated vsize (Kb) 13124 [startup+420.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2594 0 0 0 41967 17 0 0 25 0 1 0 1843340204 11427840 2580 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2790 2580 145 145 0 2645 0 [pid=1976] vsize: 11160 Current children cumulated CPU time (s) 419.84 Current children cumulated vsize (Kb) 13284 [startup+430.032 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2701 0 0 0 42965 18 0 0 25 0 1 0 1843340204 11870208 2687 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2898 2687 145 145 0 2753 0 [pid=1976] vsize: 11592 Current children cumulated CPU time (s) 429.83 Current children cumulated vsize (Kb) 13716 [startup+440.033 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2721 0 0 0 43965 18 0 0 25 0 1 0 1843340204 11968512 2707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2922 2707 145 145 0 2777 0 [pid=1976] vsize: 11688 Current children cumulated CPU time (s) 439.83 Current children cumulated vsize (Kb) 13812 [startup+450.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2722 0 0 0 44966 18 0 0 25 0 1 0 1843340204 11968512 2708 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2922 2708 145 145 0 2777 0 [pid=1976] vsize: 11688 Current children cumulated CPU time (s) 449.84 Current children cumulated vsize (Kb) 13812 [startup+460.034 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2737 0 0 0 45966 18 0 0 25 0 1 0 1843340204 12050432 2723 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2942 2723 145 145 0 2797 0 [pid=1976] vsize: 11768 Current children cumulated CPU time (s) 459.84 Current children cumulated vsize (Kb) 13892 [startup+470.035 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2744 0 0 0 46966 18 0 0 25 0 1 0 1843340204 12075008 2730 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 2948 2730 145 145 0 2803 0 [pid=1976] vsize: 11792 Current children cumulated CPU time (s) 469.84 Current children cumulated vsize (Kb) 13916 [startup+480.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2851 0 0 0 47964 19 0 0 25 0 1 0 1843340204 12525568 2837 4294967295 134512640 135094434 3221224448 3221223104 134558022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3058 2837 145 145 0 2913 0 [pid=1976] vsize: 12232 Current children cumulated CPU time (s) 479.83 Current children cumulated vsize (Kb) 14356 [startup+490.036 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2885 0 0 0 48963 19 0 0 25 0 1 0 1843340204 12681216 2871 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3096 2871 145 145 0 2951 0 [pid=1976] vsize: 12384 Current children cumulated CPU time (s) 489.82 Current children cumulated vsize (Kb) 14508 [startup+500.037 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2943 0 0 0 49962 20 0 0 25 0 1 0 1843340204 12926976 2929 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3156 2929 145 145 0 3011 0 [pid=1976] vsize: 12624 Current children cumulated CPU time (s) 499.82 Current children cumulated vsize (Kb) 14748 [startup+510.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2946 0 0 0 50963 20 0 0 25 0 1 0 1843340204 12943360 2932 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3160 2932 145 145 0 3015 0 [pid=1976] vsize: 12640 Current children cumulated CPU time (s) 509.83 Current children cumulated vsize (Kb) 14764 [startup+520.038 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2947 0 0 0 51963 20 0 0 25 0 1 0 1843340204 12943360 2933 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3160 2933 145 145 0 3015 0 [pid=1976] vsize: 12640 Current children cumulated CPU time (s) 519.83 Current children cumulated vsize (Kb) 14764 [startup+530.039 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2947 0 0 0 52963 20 0 0 25 0 1 0 1843340204 12943360 2933 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3160 2933 145 145 0 3015 0 [pid=1976] vsize: 12640 Current children cumulated CPU time (s) 529.83 Current children cumulated vsize (Kb) 14764 [startup+540.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2958 0 0 0 53963 20 0 0 25 0 1 0 1843340204 13008896 2944 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3176 2944 145 145 0 3031 0 [pid=1976] vsize: 12704 Current children cumulated CPU time (s) 539.83 Current children cumulated vsize (Kb) 14828 [startup+550.04 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2961 0 0 0 54963 20 0 0 25 0 1 0 1843340204 13008896 2947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3176 2947 145 145 0 3031 0 [pid=1976] vsize: 12704 Current children cumulated CPU time (s) 549.83 Current children cumulated vsize (Kb) 14828 [startup+560.041 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2961 0 0 0 55963 20 0 0 25 0 1 0 1843340204 13008896 2947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3176 2947 145 145 0 3031 0 [pid=1976] vsize: 12704 Current children cumulated CPU time (s) 559.83 Current children cumulated vsize (Kb) 14828 [startup+570.042 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2993 0 0 0 56964 20 0 0 25 0 1 0 1843340204 13164544 2979 4294967295 134512640 135094434 3221224448 3221223040 134551463 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3214 2979 145 145 0 3069 0 [pid=1976] vsize: 12856 Current children cumulated CPU time (s) 569.84 Current children cumulated vsize (Kb) 14980 [startup+580.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 57963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0 [pid=1976] vsize: 12888 Current children cumulated CPU time (s) 579.83 Current children cumulated vsize (Kb) 15012 [startup+590.043 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 58963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223040 134552132 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0 [pid=1976] vsize: 12888 Current children cumulated CPU time (s) 589.83 Current children cumulated vsize (Kb) 15012 [startup+600.044 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 59963 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223040 134557404 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0 [pid=1976] vsize: 12888 Current children cumulated CPU time (s) 599.83 Current children cumulated vsize (Kb) 15012 [startup+610.045 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 2998 0 0 0 60964 20 0 0 25 0 1 0 1843340204 13197312 2984 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3222 2984 145 145 0 3077 0 [pid=1976] vsize: 12888 Current children cumulated CPU time (s) 609.84 Current children cumulated vsize (Kb) 15012 [startup+620.046 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3007 0 0 0 61964 20 0 0 25 0 1 0 1843340204 13238272 2993 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3232 2993 145 145 0 3087 0 [pid=1976] vsize: 12928 Current children cumulated CPU time (s) 619.84 Current children cumulated vsize (Kb) 15052 [startup+630.047 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3169 0 0 0 62961 21 0 0 25 0 1 0 1843340204 13926400 3155 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3400 3155 145 145 0 3255 0 [pid=1976] vsize: 13600 Current children cumulated CPU time (s) 629.82 Current children cumulated vsize (Kb) 15724 [startup+640.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3201 0 0 0 63961 22 0 0 25 0 1 0 1843340204 14057472 3187 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3432 3187 145 145 0 3287 0 [pid=1976] vsize: 13728 Current children cumulated CPU time (s) 639.83 Current children cumulated vsize (Kb) 15852 [startup+650.049 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3204 0 0 0 64961 22 0 0 25 0 1 0 1843340204 14069760 3190 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3435 3190 145 145 0 3290 0 [pid=1976] vsize: 13740 Current children cumulated CPU time (s) 649.83 Current children cumulated vsize (Kb) 15864 [startup+660.051 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3205 0 0 0 65961 22 0 0 25 0 1 0 1843340204 14069760 3191 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3435 3191 145 145 0 3290 0 [pid=1976] vsize: 13740 Current children cumulated CPU time (s) 659.83 Current children cumulated vsize (Kb) 15864 [startup+670.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3205 0 0 0 66962 22 0 0 25 0 1 0 1843340204 14069760 3191 4294967295 134512640 135094434 3221224448 3221223040 134551997 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3435 3191 145 145 0 3290 0 [pid=1976] vsize: 13740 Current children cumulated CPU time (s) 669.84 Current children cumulated vsize (Kb) 15864 [startup+680.052 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3294 0 0 0 67960 22 0 0 25 0 1 0 1843340204 14467072 3280 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3532 3280 145 145 0 3387 0 [pid=1976] vsize: 14128 Current children cumulated CPU time (s) 679.82 Current children cumulated vsize (Kb) 16252 [startup+690.053 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3298 0 0 0 68961 22 0 0 25 0 1 0 1843340204 14483456 3284 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3536 3284 145 145 0 3391 0 [pid=1976] vsize: 14144 Current children cumulated CPU time (s) 689.83 Current children cumulated vsize (Kb) 16268 [startup+700.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3303 0 0 0 69961 22 0 0 25 0 1 0 1843340204 14516224 3289 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3544 3289 145 145 0 3399 0 [pid=1976] vsize: 14176 Current children cumulated CPU time (s) 699.83 Current children cumulated vsize (Kb) 16300 [startup+710.054 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 70961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0 [pid=1976] vsize: 14304 Current children cumulated CPU time (s) 709.84 Current children cumulated vsize (Kb) 16428 [startup+720.055 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 71961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0 [pid=1976] vsize: 14304 Current children cumulated CPU time (s) 719.84 Current children cumulated vsize (Kb) 16428 [startup+730.056 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 72961 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0 [pid=1976] vsize: 14304 Current children cumulated CPU time (s) 729.84 Current children cumulated vsize (Kb) 16428 [startup+740.056 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 73962 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223040 134551465 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0 [pid=1976] vsize: 14304 Current children cumulated CPU time (s) 739.85 Current children cumulated vsize (Kb) 16428 [startup+750.057 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3326 0 0 0 74962 23 0 0 25 0 1 0 1843340204 14647296 3312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3576 3312 145 145 0 3431 0 [pid=1976] vsize: 14304 Current children cumulated CPU time (s) 749.85 Current children cumulated vsize (Kb) 16428 [startup+760.059 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3521 0 0 0 75958 24 0 0 25 0 1 0 1843340204 15454208 3507 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3773 3507 145 145 0 3628 0 [pid=1976] vsize: 15092 Current children cumulated CPU time (s) 759.82 Current children cumulated vsize (Kb) 17216 [startup+770.059 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3702 0 0 0 76955 25 0 0 25 0 1 0 1843340204 16273408 3688 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3973 3688 145 145 0 3828 0 [pid=1976] vsize: 15892 Current children cumulated CPU time (s) 769.8 Current children cumulated vsize (Kb) 18016 [startup+780.06 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 77955 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 779.81 Current children cumulated vsize (Kb) 18048 [startup+790.061 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 78956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 789.82 Current children cumulated vsize (Kb) 18048 [startup+800.061 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 79956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 799.82 Current children cumulated vsize (Kb) 18048 [startup+810.062 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 80956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 809.82 Current children cumulated vsize (Kb) 18048 [startup+820.063 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 81956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 819.82 Current children cumulated vsize (Kb) 18048 [startup+830.063 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 82956 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 829.82 Current children cumulated vsize (Kb) 18048 [startup+840.064 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3711 0 0 0 83957 26 0 0 25 0 1 0 1843340204 16306176 3697 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3697 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 839.83 Current children cumulated vsize (Kb) 18048 [startup+850.065 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 84957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 849.83 Current children cumulated vsize (Kb) 18048 [startup+860.066 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 85957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223120 134556460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 859.83 Current children cumulated vsize (Kb) 18048 [startup+870.066 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 86957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557856 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 869.83 Current children cumulated vsize (Kb) 18048 [startup+880.067 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 87958 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223120 134556198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 879.84 Current children cumulated vsize (Kb) 18048 [startup+890.068 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3712 0 0 0 88957 26 0 0 25 0 1 0 1843340204 16306176 3698 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3698 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 889.83 Current children cumulated vsize (Kb) 18048 [startup+900.069 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3713 0 0 0 89957 26 0 0 25 0 1 0 1843340204 16306176 3699 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 3981 3699 145 145 0 3836 0 [pid=1976] vsize: 15924 Current children cumulated CPU time (s) 899.83 Current children cumulated vsize (Kb) 18048 [startup+910.07 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3857 0 0 0 90955 27 0 0 25 0 1 0 1843340204 16912384 3843 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4129 3843 145 145 0 3984 0 [pid=1976] vsize: 16516 Current children cumulated CPU time (s) 909.82 Current children cumulated vsize (Kb) 18640 [startup+920.071 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3916 0 0 0 91954 27 0 0 25 0 1 0 1843340204 17178624 3902 4294967295 134512640 135094434 3221224448 3221223104 134557984 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4194 3902 145 145 0 4049 0 [pid=1976] vsize: 16776 Current children cumulated CPU time (s) 919.81 Current children cumulated vsize (Kb) 18900 [startup+930.07 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3929 0 0 0 92955 27 0 0 25 0 1 0 1843340204 17260544 3915 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4214 3915 145 145 0 4069 0 [pid=1976] vsize: 16856 Current children cumulated CPU time (s) 929.82 Current children cumulated vsize (Kb) 18980 [startup+940.072 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3942 0 0 0 93955 27 0 0 25 0 1 0 1843340204 17326080 3928 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4230 3928 145 145 0 4085 0 [pid=1976] vsize: 16920 Current children cumulated CPU time (s) 939.82 Current children cumulated vsize (Kb) 19044 [startup+950.073 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3953 0 0 0 94955 27 0 0 25 0 1 0 1843340204 17391616 3939 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4246 3939 145 145 0 4101 0 [pid=1976] vsize: 16984 Current children cumulated CPU time (s) 949.82 Current children cumulated vsize (Kb) 19108 [startup+960.073 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3954 0 0 0 95955 27 0 0 25 0 1 0 1843340204 17391616 3940 4294967295 134512640 135094434 3221224448 3221223120 134556543 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4246 3940 145 145 0 4101 0 [pid=1976] vsize: 16984 Current children cumulated CPU time (s) 959.82 Current children cumulated vsize (Kb) 19108 [startup+970.074 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3954 0 0 0 96956 27 0 0 25 0 1 0 1843340204 17391616 3940 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4246 3940 145 145 0 4101 0 [pid=1976] vsize: 16984 Current children cumulated CPU time (s) 969.83 Current children cumulated vsize (Kb) 19108 [startup+980.075 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3960 0 0 0 97956 27 0 0 25 0 1 0 1843340204 17424384 3946 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4254 3946 145 145 0 4109 0 [pid=1976] vsize: 17016 Current children cumulated CPU time (s) 979.83 Current children cumulated vsize (Kb) 19140 [startup+990.075 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 98956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 989.83 Current children cumulated vsize (Kb) 19172 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 99956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 999.83 Current children cumulated vsize (Kb) 19172 [startup+1010.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 100956 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223040 134557398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 1009.83 Current children cumulated vsize (Kb) 19172 [startup+1020.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 101957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 1019.84 Current children cumulated vsize (Kb) 19172 [startup+1030.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 102957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 1029.84 Current children cumulated vsize (Kb) 19172 [startup+1040.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3966 0 0 0 103957 27 0 0 25 0 1 0 1843340204 17457152 3952 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4262 3952 145 145 0 4117 0 [pid=1976] vsize: 17048 Current children cumulated CPU time (s) 1039.84 Current children cumulated vsize (Kb) 19172 [startup+1050.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 104957 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0 [pid=1976] vsize: 17080 Current children cumulated CPU time (s) 1049.84 Current children cumulated vsize (Kb) 19204 [startup+1060.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 105958 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0 [pid=1976] vsize: 17080 Current children cumulated CPU time (s) 1059.85 Current children cumulated vsize (Kb) 19204 [startup+1070.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 3971 0 0 0 106958 27 0 0 25 0 1 0 1843340204 17489920 3957 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4270 3957 145 145 0 4125 0 [pid=1976] vsize: 17080 Current children cumulated CPU time (s) 1069.85 Current children cumulated vsize (Kb) 19204 [startup+1080.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4105 0 0 0 107956 29 0 0 25 0 1 0 1843340204 18051072 4091 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1976/statm): 4407 4091 145 145 0 4262 0 [pid=1976] vsize: 17628 Current children cumulated CPU time (s) 1079.85 Current children cumulated vsize (Kb) 19752 [startup+1090.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4117 0 0 0 108955 29 0 0 25 0 1 0 1843340204 18104320 4103 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4420 4103 145 145 0 4275 0 [pid=1976] vsize: 17680 Current children cumulated CPU time (s) 1089.84 Current children cumulated vsize (Kb) 19804 [startup+1100.08 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4132 0 0 0 109955 29 0 0 25 0 1 0 1843340204 18169856 4118 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4118 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1099.84 Current children cumulated vsize (Kb) 19868 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 110955 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1109.84 Current children cumulated vsize (Kb) 19868 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 111955 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1119.84 Current children cumulated vsize (Kb) 19868 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 112956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1129.85 Current children cumulated vsize (Kb) 19868 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 113956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1139.85 Current children cumulated vsize (Kb) 19868 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4133 0 0 0 114956 29 0 0 25 0 1 0 1843340204 18169856 4119 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4436 4119 145 145 0 4291 0 [pid=1976] vsize: 17744 Current children cumulated CPU time (s) 1149.85 Current children cumulated vsize (Kb) 19868 [startup+1160.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4141 0 0 0 115956 29 0 0 25 0 1 0 1843340204 18202624 4127 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4444 4127 145 145 0 4299 0 [pid=1976] vsize: 17776 Current children cumulated CPU time (s) 1159.85 Current children cumulated vsize (Kb) 19900 [startup+1170.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4156 0 0 0 116957 29 0 0 25 0 1 0 1843340204 18284544 4142 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4464 4142 145 145 0 4319 0 [pid=1976] vsize: 17856 Current children cumulated CPU time (s) 1169.86 Current children cumulated vsize (Kb) 19980 [startup+1180.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4156 0 0 0 117957 29 0 0 25 0 1 0 1843340204 18284544 4142 4294967295 134512640 135094434 3221224448 3221223040 134784942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4464 4142 145 145 0 4319 0 [pid=1976] vsize: 17856 Current children cumulated CPU time (s) 1179.86 Current children cumulated vsize (Kb) 19980 [startup+1190.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4163 0 0 0 118957 29 0 0 25 0 1 0 1843340204 18300928 4149 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4468 4149 145 145 0 4323 0 [pid=1976] vsize: 17872 Current children cumulated CPU time (s) 1189.86 Current children cumulated vsize (Kb) 19996 [startup+1200.09 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 119957 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0 [pid=1976] vsize: 17920 Current children cumulated CPU time (s) 1199.86 Current children cumulated vsize (Kb) 20044 [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 120958 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0 [pid=1976] vsize: 17920 Current children cumulated CPU time (s) 1209.87 Current children cumulated vsize (Kb) 20044 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.99 2/57 1976 Raw data (/proc/1972/stat): 1972 (minisat+_script) S 1971 1972 20115 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843340199 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/1972/statm): 531 226 485 147 0 384 0 [pid=1972] vsize: 2124 Raw data (/proc/1976/stat): 1976 (minisat+_64-bit) R 1972 1972 20115 0 -1 0 4172 0 0 0 120958 29 0 0 25 0 1 0 1843340204 18350080 4158 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1976/statm): 4480 4158 145 145 0 4335 0 [pid=1976] vsize: 17920 Current children cumulated CPU time (s) 1209.87 Current children cumulated vsize (Kb) 20044 Sending SIGTERM to -1972 Sleeping 2 seconds One traced child (pid=1972) ended because it received signal 15 (SIGTERM) One traced child (pid=1976) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.89 CPU user time (s): 1209.58 CPU system time (s): 0.304953 CPU usage (%): 99.9816 Max. virtual memory (cumulated for all children) (Kb): 20044
ERROR: no interpretation found !