Name | submitted/manquinho/primes-dimacs-cnf/normalized-ii8a2.opb |
MD5SUM | 6005a01d3f2ae55b0ca9c19f876c5827 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 139 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 360 |
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 | 360 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 360 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.02 |
Number of variables | 360 |
Total number of constraints | 980 |
Number of constraints which are clauses | 980 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 8 |
LAUNCH ON wulflinc3 THE 2005-09-18 15:23:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2500 boxname=wulflinc3 idbench=156 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6005a01d3f2ae55b0ca9c19f876c5827 /oldhome/oroussel/tmp/wulflinc3/normalized-ii8a2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc3/normalized-ii8a2.opb IDLAUNCH: 2500 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 957088 kB Buffers: 33976 kB Cached: 17936 kB SwapCached: 856 kB Active: 48992 kB Inactive: 5564 kB HighTotal: 131008 kB HighFree: 111468 kB LowTotal: 903652 kB LowFree: 845620 kB SwapTotal: 2097136 kB SwapFree: 2095712 kB Dirty: 0 kB Writeback: 0 kB Mapped: 5720 kB Slab: 17328 kB Committed_AS: 72324 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 15:43:36 (client local time) WITH STATUS 10 IN 1209.78 SECONDS stats: 2500 7 1209.78 10
c Parsing PB file... c Converting 980 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 | 980 2412 | 326 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 150[0m c ---[ 0]---> Sorter-cost:13276 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3 | 16839 39488 | 5613 3 20 6.7 | 0.000 % | c | 103 | 16491 38744 | 6174 90 1250 13.9 | 1.915 % | c | 254 | 16341 38418 | 6791 234 5528 23.6 | 2.729 % | c | 479 | 16038 37759 | 7470 450 11949 26.6 | 4.320 % | c | 817 | 15269 36066 | 8217 770 24110 31.3 | 8.575 % | c | 1323 | 15221 35960 | 9039 1275 41757 32.8 | 8.844 % | c | 2082 | 15221 35960 | 9943 2034 93705 46.1 | 8.844 % | c ============================================================================== c [1mFound solution: 148[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2350 | 15217 35960 | 5072 2302 101593 44.1 | 8.844 % | c | 2450 | 15217 35960 | 5579 2402 105288 43.8 | 9.084 % | c | 2600 | 15217 35960 | 6137 2552 107574 42.2 | 9.084 % | c ============================================================================== c [1mFound solution: 142[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2813 | 15257 36064 | 5085 2763 111341 40.3 | 9.084 % | c | 2915 | 15257 36064 | 5593 2865 112507 39.3 | 9.266 % | c | 3065 | 15257 36064 | 6152 3015 115583 38.3 | 9.266 % | c | 3290 | 15213 35964 | 6768 3239 129038 39.8 | 9.524 % | c | 3631 | 15119 35756 | 7444 3575 143929 40.3 | 10.048 % | c | 4137 | 15119 35756 | 8189 4081 159776 39.2 | 10.048 % | c | 4896 | 15119 35756 | 9008 4840 198324 41.0 | 10.048 % | c | 6037 | 15119 35756 | 9909 5981 259812 43.4 | 10.048 % | c | 7746 | 15119 35756 | 10900 7690 319662 41.6 | 10.048 % | c | 10309 | 15020 35539 | 11990 10251 449968 43.9 | 10.590 % | c | 14154 | 15020 35539 | 13189 7241 321460 44.4 | 10.590 % | c | 19920 | 14964 35421 | 14508 13006 623303 47.9 | 10.875 % | c ============================================================================== c [1mFound solution: 141[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27771 | 14986 35486 | 4995 11967 651063 54.4 | 10.875 % | c | 27872 | 14986 35486 | 5494 6085 308059 50.6 | 10.927 % | c | 28024 | 14931 35351 | 6043 6229 312203 50.1 | 11.294 % | c | 28250 | 14825 35119 | 6648 6439 321374 49.9 | 11.853 % | c | 28588 | 14825 35119 | 7313 6777 330987 48.8 | 11.853 % | c | 29095 | 14825 35119 | 8044 7284 349008 47.9 | 11.853 % | c | 29854 | 14825 35119 | 8848 8043 376752 46.8 | 11.853 % | c | 30994 | 14825 35119 | 9733 9183 417078 45.4 | 11.853 % | c | 32702 | 14791 35041 | 10707 10887 478885 44.0 | 12.055 % | c | 35264 | 14791 35041 | 11777 7145 253382 35.5 | 12.055 % | c | 39109 | 14791 35041 | 12955 10990 474654 43.2 | 12.055 % | c | 44877 | 14791 35041 | 14251 9411 454007 48.2 | 12.055 % | c | 53527 | 14791 35041 | 15676 9296 440843 47.4 | 12.055 % | c | 66501 | 14791 35041 | 17244 12660 591539 46.7 | 12.055 % | c | 85962 | 14752 34954 | 18968 12206 509154 41.7 | 12.275 % | c | 115155 | 14752 34954 | 20865 19570 994956 50.8 | 12.275 % | c | 158944 | 14752 34954 | 22951 15966 812506 50.9 | 12.275 % | c | 224628 | 14752 34954 | 25247 16504 780085 47.3 | 12.275 % | c ============================================================================== c [1mFound solution: 139[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 273203 | 14737 34933 | 4912 22747 1178259 51.8 | 12.275 % | c | 273303 | 14737 34933 | 5403 5787 220361 38.1 | 12.486 % | c | 273453 | 14737 34933 | 5943 5937 224417 37.8 | 12.486 % | c | 273678 | 14673 34785 | 6537 6143 232659 37.9 | 12.871 % | c | 274016 | 14673 34785 | 7191 6481 247623 38.2 | 12.871 % | c | 274524 | 14673 34785 | 7910 6989 269613 38.6 | 12.871 % | c | 275284 | 14673 34785 | 8701 7749 306748 39.6 | 12.871 % | c | 276423 | 14673 34785 | 9572 8888 356210 40.1 | 12.871 % | c | 278132 | 14636 34702 | 10529 10596 451584 42.6 | 13.082 % | c | 280694 | 14636 34702 | 11582 6651 294921 44.3 | 13.082 % | c | 284538 | 14636 34702 | 12740 10495 503132 47.9 | 13.082 % | c | 290305 | 14636 34702 | 14014 8572 373798 43.6 | 13.082 % | c | 298954 | 14636 34702 | 15415 8671 427916 49.4 | 13.082 % | c | 311928 | 14567 34547 | 16957 12461 746270 59.9 | 13.476 % | c | 331389 | 14567 34547 | 18653 12412 552554 44.5 | 13.476 % | c | 360584 | 14567 34547 | 20518 20300 1026218 50.6 | 13.476 % | c | 404373 | 14567 34547 | 22570 17926 952975 53.2 | 13.476 % | c | 470057 | 14567 34547 | 24827 21071 1096971 52.1 | 13.476 % | c | 568587 | 14539 34481 | 27310 23204 1046969 45.1 | 13.650 % |
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/18430/stat): 18430 (minisat+_script) R 18429 18430 31915 0 -1 0 19 0 0 0 0 0 0 0 19 0 1 0 1784066826 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/18430/statm): 174 3 169 147 0 27 0 [pid=18430] 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=18431 New process pid=18432 New process pid=18433 One traced child (pid=18432) exited with status: 0 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=18433) exited with status: 0 One traced child (pid=18431) exited with status: 0 New process pid=18434 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-ii8a2.opb [startup+10.0053 s] Raw data (loadavg): 0.23 0.05 0.02 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1490 0 2 0 974 7 0 0 25 0 1 0 1784066831 6578176 1431 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 1606 1431 145 145 0 1461 0 [pid=18434] vsize: 6424 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 8548 [startup+20.0071 s] Raw data (loadavg): 0.34 0.08 0.02 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1803 0 2 0 1967 10 0 0 25 0 1 0 1784066831 7839744 1744 4294967295 134512640 135094434 3221224448 3221223120 134556068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 1914 1744 145 145 0 1769 0 [pid=18434] vsize: 7656 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 9780 [startup+30.008 s] Raw data (loadavg): 0.44 0.11 0.03 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 1956 0 2 0 2965 11 0 0 25 0 1 0 1784066831 8462336 1897 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 2066 1897 145 145 0 1921 0 [pid=18434] vsize: 8264 Current children cumulated CPU time (s) 29.78 Current children cumulated vsize (Kb) 10388 [startup+40.0078 s] Raw data (loadavg): 0.53 0.14 0.04 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2142 0 2 0 3959 14 0 0 25 0 1 0 1784066831 9273344 2083 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 2264 2083 145 145 0 2119 0 [pid=18434] vsize: 9056 Current children cumulated CPU time (s) 39.75 Current children cumulated vsize (Kb) 11180 [startup+50.0096 s] Raw data (loadavg): 0.60 0.17 0.05 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 4958 14 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0 [pid=18434] vsize: 9072 Current children cumulated CPU time (s) 49.74 Current children cumulated vsize (Kb) 11196 [startup+60.0094 s] Raw data (loadavg): 0.66 0.20 0.06 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 5958 15 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0 [pid=18434] vsize: 9072 Current children cumulated CPU time (s) 59.75 Current children cumulated vsize (Kb) 11196 [startup+70.0103 s] Raw data (loadavg): 0.71 0.22 0.07 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2147 0 2 0 6958 15 0 0 25 0 1 0 1784066831 9289728 2088 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2268 2088 145 145 0 2123 0 [pid=18434] vsize: 9072 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 11196 [startup+80.0111 s] Raw data (loadavg): 0.76 0.25 0.08 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2159 0 2 0 7958 15 0 0 25 0 1 0 1784066831 9338880 2100 4294967295 134512640 135094434 3221224448 3221223040 134557131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2280 2100 145 145 0 2135 0 [pid=18434] vsize: 9120 Current children cumulated CPU time (s) 79.75 Current children cumulated vsize (Kb) 11244 [startup+90.0109 s] Raw data (loadavg): 0.79 0.27 0.09 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2265 0 2 0 8956 16 0 0 25 0 1 0 1784066831 9773056 2206 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2386 2206 145 145 0 2241 0 [pid=18434] vsize: 9544 Current children cumulated CPU time (s) 89.74 Current children cumulated vsize (Kb) 11668 [startup+100.012 s] Raw data (loadavg): 0.83 0.29 0.10 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2294 0 2 0 9956 16 0 0 25 0 1 0 1784066831 9928704 2235 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2424 2235 145 145 0 2279 0 [pid=18434] vsize: 9696 Current children cumulated CPU time (s) 99.74 Current children cumulated vsize (Kb) 11820 [startup+110.013 s] Raw data (loadavg): 0.85 0.32 0.11 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2418 0 2 0 10954 17 0 0 25 0 1 0 1784066831 10420224 2359 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2544 2359 145 145 0 2399 0 [pid=18434] vsize: 10176 Current children cumulated CPU time (s) 109.73 Current children cumulated vsize (Kb) 12300 [startup+120.013 s] Raw data (loadavg): 0.87 0.34 0.12 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2426 0 2 0 11954 17 0 0 25 0 1 0 1784066831 10452992 2367 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2552 2367 145 145 0 2407 0 [pid=18434] vsize: 10208 Current children cumulated CPU time (s) 119.73 Current children cumulated vsize (Kb) 12332 [startup+130.014 s] Raw data (loadavg): 0.89 0.36 0.13 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2556 0 2 0 12951 18 0 0 25 0 1 0 1784066831 10989568 2497 4294967295 134512640 135094434 3221224448 3221223120 134555590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2683 2497 145 145 0 2538 0 [pid=18434] vsize: 10732 Current children cumulated CPU time (s) 129.71 Current children cumulated vsize (Kb) 12856 [startup+140.014 s] Raw data (loadavg): 0.91 0.38 0.14 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2558 0 2 0 13951 18 0 0 25 0 1 0 1784066831 11001856 2499 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2686 2499 145 145 0 2541 0 [pid=18434] vsize: 10744 Current children cumulated CPU time (s) 139.71 Current children cumulated vsize (Kb) 12868 [startup+150.015 s] Raw data (loadavg): 0.92 0.40 0.15 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2562 0 2 0 14951 18 0 0 25 0 1 0 1784066831 11018240 2503 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2690 2503 145 145 0 2545 0 [pid=18434] vsize: 10760 Current children cumulated CPU time (s) 149.71 Current children cumulated vsize (Kb) 12884 [startup+160.015 s] Raw data (loadavg): 0.93 0.42 0.15 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2562 0 2 0 15951 18 0 0 25 0 1 0 1784066831 11018240 2503 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2690 2503 145 145 0 2545 0 [pid=18434] vsize: 10760 Current children cumulated CPU time (s) 159.71 Current children cumulated vsize (Kb) 12884 [startup+170.016 s] Raw data (loadavg): 0.94 0.44 0.16 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2600 0 2 0 16951 19 0 0 25 0 1 0 1784066831 11169792 2541 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2727 2541 145 145 0 2582 0 [pid=18434] vsize: 10908 Current children cumulated CPU time (s) 169.72 Current children cumulated vsize (Kb) 13032 [startup+180.016 s] Raw data (loadavg): 0.95 0.46 0.17 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2612 0 2 0 17951 19 0 0 25 0 1 0 1784066831 11223040 2553 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2740 2553 145 145 0 2595 0 [pid=18434] vsize: 10960 Current children cumulated CPU time (s) 179.72 Current children cumulated vsize (Kb) 13084 [startup+190.016 s] Raw data (loadavg): 0.96 0.47 0.18 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2770 0 2 0 18948 21 0 0 25 0 1 0 1784066831 11870208 2711 4294967295 134512640 135094434 3221224448 3221223040 134557227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2898 2711 145 145 0 2753 0 [pid=18434] vsize: 11592 Current children cumulated CPU time (s) 189.71 Current children cumulated vsize (Kb) 13716 [startup+200.017 s] Raw data (loadavg): 0.96 0.49 0.19 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2795 0 2 0 19948 21 0 0 25 0 1 0 1784066831 11980800 2736 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2925 2736 145 145 0 2780 0 [pid=18434] vsize: 11700 Current children cumulated CPU time (s) 199.71 Current children cumulated vsize (Kb) 13824 [startup+210.017 s] Raw data (loadavg): 0.97 0.51 0.20 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2812 0 2 0 20948 21 0 0 25 0 1 0 1784066831 12046336 2753 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2941 2753 145 145 0 2796 0 [pid=18434] vsize: 11764 Current children cumulated CPU time (s) 209.71 Current children cumulated vsize (Kb) 13888 [startup+220.018 s] Raw data (loadavg): 0.97 0.52 0.20 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2832 0 2 0 21948 21 0 0 25 0 1 0 1784066831 12140544 2773 4294967295 134512640 135094434 3221224448 3221222912 134781514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2964 2773 145 145 0 2819 0 [pid=18434] vsize: 11856 Current children cumulated CPU time (s) 219.71 Current children cumulated vsize (Kb) 13980 [startup+230.019 s] Raw data (loadavg): 0.98 0.54 0.21 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2832 0 2 0 22948 21 0 0 25 0 1 0 1784066831 12140544 2773 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 2964 2773 145 145 0 2819 0 [pid=18434] vsize: 11856 Current children cumulated CPU time (s) 229.71 Current children cumulated vsize (Kb) 13980 [startup+240.018 s] Raw data (loadavg): 0.98 0.55 0.22 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2937 0 2 0 23948 21 0 0 25 0 1 0 1784066831 12570624 2878 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3069 2878 145 145 0 2924 0 [pid=18434] vsize: 12276 Current children cumulated CPU time (s) 239.71 Current children cumulated vsize (Kb) 14400 [startup+250.019 s] Raw data (loadavg): 0.98 0.57 0.23 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 2954 0 2 0 24948 21 0 0 25 0 1 0 1784066831 12652544 2895 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3089 2895 145 145 0 2944 0 [pid=18434] vsize: 12356 Current children cumulated CPU time (s) 249.71 Current children cumulated vsize (Kb) 14480 [startup+260.02 s] Raw data (loadavg): 0.98 0.58 0.24 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3036 0 2 0 25947 22 0 0 25 0 1 0 1784066831 13012992 2977 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3177 2977 145 145 0 3032 0 [pid=18434] vsize: 12708 Current children cumulated CPU time (s) 259.71 Current children cumulated vsize (Kb) 14832 [startup+270.021 s] Raw data (loadavg): 0.99 0.59 0.24 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3146 0 2 0 26945 23 0 0 25 0 1 0 1784066831 13459456 3087 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3286 3087 145 145 0 3141 0 [pid=18434] vsize: 13144 Current children cumulated CPU time (s) 269.7 Current children cumulated vsize (Kb) 15268 [startup+280.022 s] Raw data (loadavg): 0.99 0.61 0.25 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3148 0 2 0 27945 23 0 0 25 0 1 0 1784066831 13471744 3089 4294967295 134512640 135094434 3221224448 3221223040 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3289 3089 145 145 0 3144 0 [pid=18434] vsize: 13156 Current children cumulated CPU time (s) 279.7 Current children cumulated vsize (Kb) 15280 [startup+290.022 s] Raw data (loadavg): 0.99 0.62 0.26 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3160 0 2 0 28945 23 0 0 25 0 1 0 1784066831 13520896 3101 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3301 3101 145 145 0 3156 0 [pid=18434] vsize: 13204 Current children cumulated CPU time (s) 289.7 Current children cumulated vsize (Kb) 15328 [startup+300.022 s] Raw data (loadavg): 0.99 0.63 0.27 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3164 0 2 0 29945 23 0 0 25 0 1 0 1784066831 13537280 3105 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 3305 3105 145 145 0 3160 0 [pid=18434] vsize: 13220 Current children cumulated CPU time (s) 299.7 Current children cumulated vsize (Kb) 15344 [startup+310.023 s] Raw data (loadavg): 0.99 0.64 0.28 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3167 0 2 0 30944 24 0 0 25 0 1 0 1784066831 13553664 3108 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3309 3108 145 145 0 3164 0 [pid=18434] vsize: 13236 Current children cumulated CPU time (s) 309.7 Current children cumulated vsize (Kb) 15360 [startup+320.025 s] Raw data (loadavg): 0.99 0.65 0.28 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3175 0 2 0 31944 24 0 0 25 0 1 0 1784066831 13586432 3116 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3317 3116 145 145 0 3172 0 [pid=18434] vsize: 13268 Current children cumulated CPU time (s) 319.7 Current children cumulated vsize (Kb) 15392 [startup+330.026 s] Raw data (loadavg): 0.99 0.67 0.29 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3190 0 2 0 32943 25 0 0 25 0 1 0 1784066831 13643776 3131 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3331 3131 145 145 0 3186 0 [pid=18434] vsize: 13324 Current children cumulated CPU time (s) 329.7 Current children cumulated vsize (Kb) 15448 [startup+340.026 s] Raw data (loadavg): 0.99 0.68 0.30 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3199 0 2 0 33943 25 0 0 25 0 1 0 1784066831 13684736 3140 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3341 3140 145 145 0 3196 0 [pid=18434] vsize: 13364 Current children cumulated CPU time (s) 339.7 Current children cumulated vsize (Kb) 15488 [startup+350.026 s] Raw data (loadavg): 0.99 0.69 0.30 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3203 0 2 0 34943 26 0 0 25 0 1 0 1784066831 13701120 3144 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3345 3144 145 145 0 3200 0 [pid=18434] vsize: 13380 Current children cumulated CPU time (s) 349.71 Current children cumulated vsize (Kb) 15504 [startup+360.026 s] Raw data (loadavg): 0.99 0.70 0.31 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3211 0 2 0 35943 26 0 0 25 0 1 0 1784066831 13733888 3152 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3353 3152 145 145 0 3208 0 [pid=18434] vsize: 13412 Current children cumulated CPU time (s) 359.71 Current children cumulated vsize (Kb) 15536 [startup+370.027 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3241 0 2 0 36942 27 0 0 25 0 1 0 1784066831 13897728 3182 4294967295 134512640 135094434 3221224448 3221223120 134555305 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3393 3182 145 145 0 3248 0 [pid=18434] vsize: 13572 Current children cumulated CPU time (s) 369.71 Current children cumulated vsize (Kb) 15696 [startup+380.028 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3245 0 2 0 37943 27 0 0 25 0 1 0 1784066831 13897728 3186 4294967295 134512640 135094434 3221224448 3221223040 134557022 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3393 3186 145 145 0 3248 0 [pid=18434] vsize: 13572 Current children cumulated CPU time (s) 379.72 Current children cumulated vsize (Kb) 15696 [startup+390.029 s] Raw data (loadavg): 0.99 0.72 0.33 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3253 0 2 0 38943 27 0 0 25 0 1 0 1784066831 13946880 3194 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3405 3194 145 145 0 3260 0 [pid=18434] vsize: 13620 Current children cumulated CPU time (s) 389.72 Current children cumulated vsize (Kb) 15744 [startup+400.03 s] Raw data (loadavg): 0.99 0.73 0.34 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3255 0 2 0 39943 27 0 0 25 0 1 0 1784066831 13946880 3196 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3405 3196 145 145 0 3260 0 [pid=18434] vsize: 13620 Current children cumulated CPU time (s) 399.72 Current children cumulated vsize (Kb) 15744 [startup+410.029 s] Raw data (loadavg): 0.99 0.74 0.34 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3256 0 2 0 40943 27 0 0 25 0 1 0 1784066831 13946880 3197 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3405 3197 145 145 0 3260 0 [pid=18434] vsize: 13620 Current children cumulated CPU time (s) 409.72 Current children cumulated vsize (Kb) 15744 [startup+420.031 s] Raw data (loadavg): 0.99 0.75 0.35 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3256 0 2 0 41943 27 0 0 25 0 1 0 1784066831 13946880 3197 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3405 3197 145 145 0 3260 0 [pid=18434] vsize: 13620 Current children cumulated CPU time (s) 419.72 Current children cumulated vsize (Kb) 15744 [startup+430.032 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 42943 27 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0 [pid=18434] vsize: 13652 Current children cumulated CPU time (s) 429.72 Current children cumulated vsize (Kb) 15776 [startup+440.033 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 43943 27 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223040 134557528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0 [pid=18434] vsize: 13652 Current children cumulated CPU time (s) 439.72 Current children cumulated vsize (Kb) 15776 [startup+450.034 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3264 0 2 0 44943 28 0 0 25 0 1 0 1784066831 13979648 3205 4294967295 134512640 135094434 3221224448 3221223040 134557512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 3413 3205 145 145 0 3268 0 [pid=18434] vsize: 13652 Current children cumulated CPU time (s) 449.73 Current children cumulated vsize (Kb) 15776 [startup+460.035 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3277 0 2 0 45942 28 0 0 25 0 1 0 1784066831 14045184 3218 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3429 3218 145 145 0 3284 0 [pid=18434] vsize: 13716 Current children cumulated CPU time (s) 459.72 Current children cumulated vsize (Kb) 15840 [startup+470.035 s] Raw data (loadavg): 0.99 0.79 0.38 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3424 0 2 0 46939 29 0 0 25 0 1 0 1784066831 14667776 3365 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3581 3365 145 145 0 3436 0 [pid=18434] vsize: 14324 Current children cumulated CPU time (s) 469.7 Current children cumulated vsize (Kb) 16448 [startup+480.036 s] Raw data (loadavg): 0.99 0.79 0.39 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3431 0 2 0 47940 29 0 0 25 0 1 0 1784066831 14700544 3372 4294967295 134512640 135094434 3221224448 3221223040 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3589 3372 145 145 0 3444 0 [pid=18434] vsize: 14356 Current children cumulated CPU time (s) 479.71 Current children cumulated vsize (Kb) 16480 [startup+490.037 s] Raw data (loadavg): 0.99 0.80 0.39 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3435 0 2 0 48940 29 0 0 25 0 1 0 1784066831 14716928 3376 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3593 3376 145 145 0 3448 0 [pid=18434] vsize: 14372 Current children cumulated CPU time (s) 489.71 Current children cumulated vsize (Kb) 16496 [startup+500.038 s] Raw data (loadavg): 0.99 0.80 0.40 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3566 0 2 0 49938 29 0 0 25 0 1 0 1784066831 15253504 3507 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3724 3507 145 145 0 3579 0 [pid=18434] vsize: 14896 Current children cumulated CPU time (s) 499.69 Current children cumulated vsize (Kb) 17020 [startup+510.038 s] Raw data (loadavg): 0.99 0.81 0.41 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3566 0 2 0 50938 30 0 0 25 0 1 0 1784066831 15253504 3507 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3724 3507 145 145 0 3579 0 [pid=18434] vsize: 14896 Current children cumulated CPU time (s) 509.7 Current children cumulated vsize (Kb) 17020 [startup+520.038 s] Raw data (loadavg): 0.99 0.82 0.41 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3567 0 2 0 51938 30 0 0 25 0 1 0 1784066831 15253504 3508 4294967295 134512640 135094434 3221224448 3221223040 134557503 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3724 3508 145 145 0 3579 0 [pid=18434] vsize: 14896 Current children cumulated CPU time (s) 519.7 Current children cumulated vsize (Kb) 17020 [startup+530.039 s] Raw data (loadavg): 0.99 0.82 0.42 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3658 0 2 0 52938 30 0 0 25 0 1 0 1784066831 15638528 3599 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3818 3599 145 145 0 3673 0 [pid=18434] vsize: 15272 Current children cumulated CPU time (s) 529.7 Current children cumulated vsize (Kb) 17396 [startup+540.039 s] Raw data (loadavg): 0.99 0.83 0.42 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 53937 30 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 539.69 Current children cumulated vsize (Kb) 17552 [startup+550.04 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 54937 30 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 549.69 Current children cumulated vsize (Kb) 17552 [startup+560.041 s] Raw data (loadavg): 0.99 0.84 0.43 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 55937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 559.7 Current children cumulated vsize (Kb) 17552 [startup+570.042 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 56937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 569.7 Current children cumulated vsize (Kb) 17552 [startup+580.043 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 57937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 579.7 Current children cumulated vsize (Kb) 17552 [startup+590.042 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 58937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 589.7 Current children cumulated vsize (Kb) 17552 [startup+600.043 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 59937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 599.7 Current children cumulated vsize (Kb) 17552 [startup+610.044 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 60937 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 609.7 Current children cumulated vsize (Kb) 17552 [startup+620.045 s] Raw data (loadavg): 0.99 0.86 0.47 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 61938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 619.71 Current children cumulated vsize (Kb) 17552 [startup+630.046 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 62938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 629.71 Current children cumulated vsize (Kb) 17552 [startup+640.046 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 63938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557810 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 639.71 Current children cumulated vsize (Kb) 17552 [startup+650.047 s] Raw data (loadavg): 0.99 0.88 0.48 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 64938 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 649.71 Current children cumulated vsize (Kb) 17552 [startup+660.047 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 65939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 659.72 Current children cumulated vsize (Kb) 17552 [startup+670.048 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 66939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 669.72 Current children cumulated vsize (Kb) 17552 [startup+680.049 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 67939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223136 134554726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 679.72 Current children cumulated vsize (Kb) 17552 [startup+690.049 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 68939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223088 134562139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 689.72 Current children cumulated vsize (Kb) 17552 [startup+700.049 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 69939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 699.72 Current children cumulated vsize (Kb) 17552 [startup+710.049 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 70939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 709.72 Current children cumulated vsize (Kb) 17552 [startup+720.05 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 71939 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 719.72 Current children cumulated vsize (Kb) 17552 [startup+730.051 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 72940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 729.73 Current children cumulated vsize (Kb) 17552 [startup+740.052 s] Raw data (loadavg): 0.99 0.90 0.53 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 73940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 739.73 Current children cumulated vsize (Kb) 17552 [startup+750.053 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 74940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 749.73 Current children cumulated vsize (Kb) 17552 [startup+760.053 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 75940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 759.73 Current children cumulated vsize (Kb) 17552 [startup+770.054 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3697 0 2 0 76940 31 0 0 25 0 1 0 1784066831 15798272 3638 4294967295 134512640 135094434 3221224448 3221223040 134551669 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3857 3638 145 145 0 3712 0 [pid=18434] vsize: 15428 Current children cumulated CPU time (s) 769.73 Current children cumulated vsize (Kb) 17552 [startup+780.055 s] Raw data (loadavg): 0.99 0.91 0.55 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3703 0 2 0 77941 31 0 0 25 0 1 0 1784066831 15831040 3644 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3865 3644 145 145 0 3720 0 [pid=18434] vsize: 15460 Current children cumulated CPU time (s) 779.74 Current children cumulated vsize (Kb) 17584 [startup+790.055 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3708 0 2 0 78941 31 0 0 25 0 1 0 1784066831 15863808 3649 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3873 3649 145 145 0 3728 0 [pid=18434] vsize: 15492 Current children cumulated CPU time (s) 789.74 Current children cumulated vsize (Kb) 17616 [startup+800.056 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3714 0 2 0 79941 31 0 0 25 0 1 0 1784066831 15896576 3655 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3881 3655 145 145 0 3736 0 [pid=18434] vsize: 15524 Current children cumulated CPU time (s) 799.74 Current children cumulated vsize (Kb) 17648 [startup+810.057 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3730 0 2 0 80941 32 0 0 25 0 1 0 1784066831 15966208 3671 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3898 3671 145 145 0 3753 0 [pid=18434] vsize: 15592 Current children cumulated CPU time (s) 809.75 Current children cumulated vsize (Kb) 17716 [startup+820.057 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3742 0 2 0 81941 32 0 0 25 0 1 0 1784066831 16019456 3683 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3911 3683 145 145 0 3766 0 [pid=18434] vsize: 15644 Current children cumulated CPU time (s) 819.75 Current children cumulated vsize (Kb) 17768 [startup+830.058 s] Raw data (loadavg): 0.99 0.92 0.57 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3743 0 2 0 82941 32 0 0 25 0 1 0 1784066831 16019456 3684 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3911 3684 145 145 0 3766 0 [pid=18434] vsize: 15644 Current children cumulated CPU time (s) 829.75 Current children cumulated vsize (Kb) 17768 [startup+840.059 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3743 0 2 0 83941 32 0 0 25 0 1 0 1784066831 16019456 3684 4294967295 134512640 135094434 3221224448 3221223104 134556602 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3911 3684 145 145 0 3766 0 [pid=18434] vsize: 15644 Current children cumulated CPU time (s) 839.75 Current children cumulated vsize (Kb) 17768 [startup+850.06 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3747 0 2 0 84942 32 0 0 25 0 1 0 1784066831 16035840 3688 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 3915 3688 145 145 0 3770 0 [pid=18434] vsize: 15660 Current children cumulated CPU time (s) 849.76 Current children cumulated vsize (Kb) 17784 [startup+860.061 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3843 0 2 0 85940 32 0 0 25 0 1 0 1784066831 16429056 3784 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4011 3784 145 145 0 3866 0 [pid=18434] vsize: 16044 Current children cumulated CPU time (s) 859.74 Current children cumulated vsize (Kb) 18168 [startup+870.062 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3856 0 2 0 86940 32 0 0 25 0 1 0 1784066831 16482304 3797 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4024 3797 145 145 0 3879 0 [pid=18434] vsize: 16096 Current children cumulated CPU time (s) 869.74 Current children cumulated vsize (Kb) 18220 [startup+880.063 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3869 0 2 0 87940 32 0 0 25 0 1 0 1784066831 16531456 3810 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4036 3810 145 145 0 3891 0 [pid=18434] vsize: 16144 Current children cumulated CPU time (s) 879.74 Current children cumulated vsize (Kb) 18268 [startup+890.063 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3897 0 2 0 88940 33 0 0 25 0 1 0 1784066831 16666624 3838 4294967295 134512640 135094434 3221224448 3221223040 134557339 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4069 3838 145 145 0 3924 0 [pid=18434] vsize: 16276 Current children cumulated CPU time (s) 889.75 Current children cumulated vsize (Kb) 18400 [startup+900.064 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3897 0 2 0 89940 33 0 0 25 0 1 0 1784066831 16666624 3838 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4069 3838 145 145 0 3924 0 [pid=18434] vsize: 16276 Current children cumulated CPU time (s) 899.75 Current children cumulated vsize (Kb) 18400 [startup+910.065 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 90940 33 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0 [pid=18434] vsize: 16300 Current children cumulated CPU time (s) 909.75 Current children cumulated vsize (Kb) 18424 [startup+920.066 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 91940 33 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0 [pid=18434] vsize: 16300 Current children cumulated CPU time (s) 919.75 Current children cumulated vsize (Kb) 18424 [startup+930.067 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3903 0 2 0 92939 34 0 0 25 0 1 0 1784066831 16691200 3844 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4075 3844 145 145 0 3930 0 [pid=18434] vsize: 16300 Current children cumulated CPU time (s) 929.75 Current children cumulated vsize (Kb) 18424 [startup+940.068 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3917 0 2 0 93939 35 0 0 25 0 1 0 1784066831 16773120 3858 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4095 3858 145 145 0 3950 0 [pid=18434] vsize: 16380 Current children cumulated CPU time (s) 939.76 Current children cumulated vsize (Kb) 18504 [startup+950.069 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3924 0 2 0 94939 35 0 0 25 0 1 0 1784066831 16805888 3865 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4103 3865 145 145 0 3958 0 [pid=18434] vsize: 16412 Current children cumulated CPU time (s) 949.76 Current children cumulated vsize (Kb) 18536 [startup+960.07 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3924 0 2 0 95939 35 0 0 25 0 1 0 1784066831 16805888 3865 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4103 3865 145 145 0 3958 0 [pid=18434] vsize: 16412 Current children cumulated CPU time (s) 959.76 Current children cumulated vsize (Kb) 18536 [startup+970.071 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3929 0 2 0 96939 36 0 0 25 0 1 0 1784066831 16838656 3870 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4111 3870 145 145 0 3966 0 [pid=18434] vsize: 16444 Current children cumulated CPU time (s) 969.77 Current children cumulated vsize (Kb) 18568 [startup+980.072 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3946 0 2 0 97939 36 0 0 25 0 1 0 1784066831 16936960 3887 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4135 3887 145 145 0 3990 0 [pid=18434] vsize: 16540 Current children cumulated CPU time (s) 979.77 Current children cumulated vsize (Kb) 18664 [startup+990.071 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3957 0 2 0 98939 36 0 0 25 0 1 0 1784066831 17002496 3898 4294967295 134512640 135094434 3221224448 3221223104 134555980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4151 3898 145 145 0 4006 0 [pid=18434] vsize: 16604 Current children cumulated CPU time (s) 989.77 Current children cumulated vsize (Kb) 18728 [startup+1000.07 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3961 0 2 0 99939 36 0 0 25 0 1 0 1784066831 17018880 3902 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4155 3902 145 145 0 4010 0 [pid=18434] vsize: 16620 Current children cumulated CPU time (s) 999.77 Current children cumulated vsize (Kb) 18744 [startup+1010.07 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3973 0 2 0 100939 36 0 0 25 0 1 0 1784066831 17084416 3914 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4171 3914 145 145 0 4026 0 [pid=18434] vsize: 16684 Current children cumulated CPU time (s) 1009.77 Current children cumulated vsize (Kb) 18808 [startup+1020.07 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3976 0 2 0 101939 37 0 0 25 0 1 0 1784066831 17100800 3917 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4175 3917 145 145 0 4030 0 [pid=18434] vsize: 16700 Current children cumulated CPU time (s) 1019.78 Current children cumulated vsize (Kb) 18824 [startup+1030.07 s] Raw data (loadavg): 1.07 0.97 0.65 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3984 0 2 0 102939 37 0 0 25 0 1 0 1784066831 17149952 3925 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4187 3925 145 145 0 4042 0 [pid=18434] vsize: 16748 Current children cumulated CPU time (s) 1029.78 Current children cumulated vsize (Kb) 18872 [startup+1040.08 s] Raw data (loadavg): 1.06 0.97 0.65 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3985 0 2 0 103939 37 0 0 25 0 1 0 1784066831 17149952 3926 4294967295 134512640 135094434 3221224448 3221223104 134557815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4187 3926 145 145 0 4042 0 [pid=18434] vsize: 16748 Current children cumulated CPU time (s) 1039.78 Current children cumulated vsize (Kb) 18872 [startup+1050.08 s] Raw data (loadavg): 1.05 0.97 0.65 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3989 0 2 0 104939 37 0 0 25 0 1 0 1784066831 17166336 3930 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4191 3930 145 145 0 4046 0 [pid=18434] vsize: 16764 Current children cumulated CPU time (s) 1049.78 Current children cumulated vsize (Kb) 18888 [startup+1060.08 s] Raw data (loadavg): 1.04 0.97 0.66 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 105939 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0 [pid=18434] vsize: 16796 Current children cumulated CPU time (s) 1059.78 Current children cumulated vsize (Kb) 18920 [startup+1070.08 s] Raw data (loadavg): 1.04 0.97 0.66 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 106939 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0 [pid=18434] vsize: 16796 Current children cumulated CPU time (s) 1069.78 Current children cumulated vsize (Kb) 18920 [startup+1080.08 s] Raw data (loadavg): 1.03 0.97 0.66 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3995 0 2 0 107940 37 0 0 25 0 1 0 1784066831 17199104 3936 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4199 3936 145 145 0 4054 0 [pid=18434] vsize: 16796 Current children cumulated CPU time (s) 1079.79 Current children cumulated vsize (Kb) 18920 [startup+1090.08 s] Raw data (loadavg): 1.03 0.97 0.66 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3998 0 2 0 108940 37 0 0 25 0 1 0 1784066831 17215488 3939 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4203 3939 145 145 0 4058 0 [pid=18434] vsize: 16812 Current children cumulated CPU time (s) 1089.79 Current children cumulated vsize (Kb) 18936 [startup+1100.08 s] Raw data (loadavg): 1.02 0.97 0.67 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 3998 0 2 0 109940 37 0 0 25 0 1 0 1784066831 17215488 3939 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4203 3939 145 145 0 4058 0 [pid=18434] vsize: 16812 Current children cumulated CPU time (s) 1099.79 Current children cumulated vsize (Kb) 18936 [startup+1110.08 s] Raw data (loadavg): 1.02 0.97 0.67 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4014 0 2 0 110940 38 0 0 25 0 1 0 1784066831 17281024 3955 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4219 3955 145 145 0 4074 0 [pid=18434] vsize: 16876 Current children cumulated CPU time (s) 1109.8 Current children cumulated vsize (Kb) 19000 [startup+1120.08 s] Raw data (loadavg): 1.01 0.97 0.67 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4026 0 2 0 111940 38 0 0 25 0 1 0 1784066831 17313792 3967 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4227 3967 145 145 0 4082 0 [pid=18434] vsize: 16908 Current children cumulated CPU time (s) 1119.8 Current children cumulated vsize (Kb) 19032 [startup+1130.08 s] Raw data (loadavg): 1.01 0.97 0.68 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4051 0 2 0 112940 38 0 0 25 0 1 0 1784066831 17440768 3992 4294967295 134512640 135094434 3221224448 3221223104 134558423 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4258 3992 145 145 0 4113 0 [pid=18434] vsize: 17032 Current children cumulated CPU time (s) 1129.8 Current children cumulated vsize (Kb) 19156 [startup+1140.08 s] Raw data (loadavg): 1.01 0.97 0.68 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4052 0 2 0 113940 38 0 0 25 0 1 0 1784066831 17440768 3993 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4258 3993 145 145 0 4113 0 [pid=18434] vsize: 17032 Current children cumulated CPU time (s) 1139.8 Current children cumulated vsize (Kb) 19156 [startup+1150.08 s] Raw data (loadavg): 1.01 0.97 0.68 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4064 0 2 0 114940 38 0 0 25 0 1 0 1784066831 17506304 4005 4294967295 134512640 135094434 3221224448 3221223040 134557287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 4274 4005 145 145 0 4129 0 [pid=18434] vsize: 17096 Current children cumulated CPU time (s) 1149.8 Current children cumulated vsize (Kb) 19220 [startup+1160.08 s] Raw data (loadavg): 1.01 0.97 0.69 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4076 0 2 0 115939 38 0 0 25 0 1 0 1784066831 17571840 4017 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/18434/statm): 4290 4017 145 145 0 4145 0 [pid=18434] vsize: 17160 Current children cumulated CPU time (s) 1159.79 Current children cumulated vsize (Kb) 19284 [startup+1170.09 s] Raw data (loadavg): 1.00 0.97 0.69 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4095 0 2 0 116938 38 0 0 25 0 1 0 1784066831 17645568 4036 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4308 4036 145 145 0 4163 0 [pid=18434] vsize: 17232 Current children cumulated CPU time (s) 1169.78 Current children cumulated vsize (Kb) 19356 [startup+1180.09 s] Raw data (loadavg): 1.00 0.97 0.69 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4098 0 2 0 117939 38 0 0 25 0 1 0 1784066831 17661952 4039 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4312 4039 145 145 0 4167 0 [pid=18434] vsize: 17248 Current children cumulated CPU time (s) 1179.79 Current children cumulated vsize (Kb) 19372 [startup+1190.09 s] Raw data (loadavg): 1.00 0.97 0.69 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4099 0 2 0 118939 38 0 0 25 0 1 0 1784066831 17661952 4040 4294967295 134512640 135094434 3221224448 3221223104 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4312 4040 145 145 0 4167 0 [pid=18434] vsize: 17248 Current children cumulated CPU time (s) 1189.79 Current children cumulated vsize (Kb) 19372 [startup+1200.09 s] Raw data (loadavg): 1.00 0.97 0.70 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4232 0 2 0 119936 40 0 0 25 0 1 0 1784066831 18210816 4173 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4446 4173 145 145 0 4301 0 [pid=18434] vsize: 17784 Current children cumulated CPU time (s) 1199.78 Current children cumulated vsize (Kb) 19908 [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.70 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4242 0 2 0 120936 40 0 0 25 0 1 0 1784066831 18255872 4183 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4457 4183 145 145 0 4312 0 [pid=18434] vsize: 17828 Current children cumulated CPU time (s) 1209.78 Current children cumulated vsize (Kb) 19952 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 0.97 0.70 2/57 18434 Raw data (/proc/18430/stat): 18430 (minisat+_script) S 18429 18430 31915 0 -1 0 288 239 0 0 0 1 0 1 19 0 1 0 1784066826 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/18430/statm): 531 226 485 147 0 384 0 [pid=18430] vsize: 2124 Raw data (/proc/18434/stat): 18434 (minisat+_64-bit) R 18430 18430 31915 0 -1 0 4242 0 2 0 120936 40 0 0 25 0 1 0 1784066831 18255872 4183 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/18434/statm): 4457 4183 145 145 0 4312 0 [pid=18434] vsize: 17828 Current children cumulated CPU time (s) 1209.78 Current children cumulated vsize (Kb) 19952 Sending SIGTERM to -18430 Sleeping 2 seconds One traced child (pid=18430) ended because it received signal 15 (SIGTERM) One traced child (pid=18434) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.1 CPU time (s): 1209.78 CPU user time (s): 1209.37 CPU system time (s): 0.414936 CPU usage (%): 99.9734 Max. virtual memory (cumulated for all children) (Kb): 19952
ERROR: no interpretation found !