Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-3.opb |
MD5SUM | 25457db86ce3cc3b7604dfa37c8096b4 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -29 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
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 | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.03 |
Number of variables | 595 |
Total number of constraints | 27931 |
Number of constraints which are clauses | 27931 |
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 | 2 |
LAUNCH ON wulflinc11 THE 2005-09-18 18:44:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2694 boxname=wulflinc11 idbench=350 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 25457db86ce3cc3b7604dfa37c8096b4 /oldhome/oroussel/tmp/wulflinc11/normalized-frb35-17-3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-frb35-17-3.opb IDLAUNCH: 2694 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.028 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 926992 kB Buffers: 31500 kB Cached: 48552 kB SwapCached: 732 kB Active: 44484 kB Inactive: 38224 kB HighTotal: 131008 kB HighFree: 80500 kB LowTotal: 903652 kB LowFree: 846492 kB SwapTotal: 2097136 kB SwapFree: 2095856 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 19140 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 19:04:19 (client local time) WITH STATUS 10 IN 1209.63 SECONDS stats: 2694 7 1209.63 10
c Parsing PB file... c Converting 27931 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 | 27931 55862 | 9310 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -25[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56226 122317 | 18742 0 0 nan | 0.000 % | c | 100 | 56017 121884 | 20616 93 1165 12.5 | 0.585 % | c | 250 | 55219 120180 | 22677 215 2505 11.7 | 2.925 % | c | 475 | 54050 117632 | 24945 366 4294 11.7 | 6.485 % | c | 813 | 52427 114064 | 27440 604 7515 12.4 | 11.657 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1312 | 49748 108075 | 16582 973 13038 13.4 | 11.657 % | c | 1412 | 49314 107081 | 18240 1047 14480 13.8 | 21.494 % | c | 1562 | 48109 104346 | 20064 1117 15274 13.7 | 25.435 % | c | 1787 | 46873 101501 | 22070 1273 17136 13.5 | 29.543 % | c | 2124 | 45440 98214 | 24277 1530 19819 13.0 | 34.301 % | c | 2630 | 43350 93367 | 26705 1845 25665 13.9 | 41.215 % | c | 3389 | 41978 90084 | 29376 2483 31539 12.7 | 45.869 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3553 | 41830 89810 | 13943 2628 34703 13.2 | 45.869 % | c | 3653 | 41490 88994 | 15337 2682 35918 13.4 | 47.845 % | c | 3803 | 41155 88218 | 16871 2808 38474 13.7 | 48.966 % | c | 4028 | 40908 87625 | 18558 2975 42154 14.2 | 49.830 % | c | 4365 | 40256 86118 | 20413 3168 49450 15.6 | 52.022 % | c | 4871 | 39264 83777 | 22455 3528 61471 17.4 | 55.427 % | c ============================================================================== c [1mFound solution: -28[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5253 | 38681 82397 | 12893 3832 66544 17.4 | 55.427 % | c | 5354 | 38557 82103 | 14182 3922 71658 18.3 | 57.906 % | c | 5504 | 38289 81462 | 15600 4018 73309 18.2 | 58.842 % | c | 5730 | 38127 81078 | 17160 4185 78516 18.8 | 59.413 % | c | 6067 | 37939 80622 | 18876 4417 84596 19.2 | 60.102 % | c | 6574 | 37077 78579 | 20764 4679 91036 19.5 | 63.065 % | c | 7334 | 36460 77108 | 22840 5284 107904 20.4 | 65.312 % | c | 8474 | 35325 74406 | 25124 6063 138814 22.9 | 69.098 % | c ============================================================================== c [1mFound solution: -29[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9550 | 35051 73788 | 11683 7007 181532 25.9 | 69.098 % | c | 9650 | 35051 73788 | 12851 7107 185723 26.1 | 70.086 % | c | 9800 | 35044 73773 | 14136 7237 189597 26.2 | 70.106 % | c | 10025 | 35044 73773 | 15550 7462 206968 27.7 | 70.106 % | c | 10362 | 34754 73089 | 17105 7671 217020 28.3 | 71.113 % | c ============================================================================== c [1mFound solution: -30[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10418 | 34746 73026 | 11582 7715 217249 28.2 | 71.113 % | c | 10519 | 34708 72936 | 12740 7766 220611 28.4 | 71.286 % | c | 10669 | 34561 72582 | 14014 7879 225784 28.7 | 71.809 % | c | 10895 | 34561 72582 | 15415 8105 234073 28.9 | 71.809 % | c | 11232 | 34503 72446 | 16957 8415 250564 29.8 | 72.010 % | c | 11738 | 34040 71355 | 18652 8744 269440 30.8 | 73.746 % | c | 12497 | 33540 70146 | 20518 9112 292045 32.1 | 75.384 % | c | 13637 | 33245 69430 | 22570 10095 339815 33.7 | 76.437 % | c | 15346 | 33103 69093 | 24827 11789 430037 36.5 | 76.935 % | c | 17908 | 32838 68436 | 27309 14169 571943 40.4 | 77.900 % | c | 21752 | 32406 67389 | 30040 17744 810159 45.7 | 79.467 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25513 | 32400 67391 | 10800 21435 1132948 52.9 | 79.467 % | c | 25613 | 32400 67391 | 11880 21535 1137302 52.8 | 79.580 % | c | 25763 | 32297 67128 | 13068 21449 1138247 53.1 | 79.974 % | c | 25988 | 32297 67128 | 14374 21674 1153380 53.2 | 79.973 % | c | 26325 | 32226 66949 | 15812 21871 1164442 53.2 | 80.245 % | c | 26832 | 32226 66949 | 17393 22378 1189285 53.1 | 80.245 % | c | 27591 | 32203 66890 | 19132 23072 1220699 52.9 | 80.337 % | c | 28731 | 32203 66890 | 21046 24212 1292326 53.4 | 80.337 % | c | 30439 | 32177 66823 | 23150 25888 1432498 55.3 | 80.439 % | c | 33002 | 32174 66816 | 25465 28443 1544015 54.3 | 80.449 % | c | 36846 | 32165 66795 | 28012 32086 1770438 55.2 | 80.480 % | c | 42612 | 32165 66795 | 30813 37852 2233106 59.0 | 80.480 % | c ============================================================================== c [1mFound solution: -32[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49852 | 32020 66434 | 10673 44908 2776824 61.8 | 80.480 % | c | 49952 | 32020 66434 | 11740 16606 965248 58.1 | 81.008 % | c | 50103 | 32020 66434 | 12914 16757 968861 57.8 | 81.008 % | c | 50328 | 32020 66434 | 14205 16982 978993 57.6 | 81.008 % | c | 50665 | 32020 66434 | 15626 17319 1003362 57.9 | 81.008 % | c | 51172 | 32020 66434 | 17188 17826 1036082 58.1 | 81.008 % | c | 51931 | 31991 66359 | 18907 18574 1086045 58.5 | 81.121 % | c | 53070 | 31649 65547 | 20798 19664 1187670 60.4 | 82.297 % | c | 54779 | 31649 65547 | 22878 21373 1349706 63.2 | 82.297 % | c | 57343 | 31614 65464 | 25166 23929 1562175 65.3 | 82.420 % | c | 61188 | 31576 65372 | 27683 27752 1803243 65.0 | 82.553 % | c | 66954 | 31574 65368 | 30451 33497 2289530 68.4 | 82.558 % | c | 75604 | 31532 65264 | 33496 42137 3056028 72.5 | 82.716 % | c | 88578 | 31532 65264 | 36846 21336 1265506 59.3 | 82.716 % | c | 108040 | 31529 65257 | 40530 40797 2591421 63.5 | 82.727 % | c | 137232 | 31529 65257 | 44583 29377 1221521 41.6 | 82.727 % | c ============================================================================== c [1mFound solution: -33[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 148357 | 31547 65303 | 10515 40502 1622760 40.1 | 82.727 % | c | 148458 | 31547 65303 | 11566 17946 543672 30.3 | 82.688 % | c | 148609 | 31547 65303 | 12723 18097 548810 30.3 | 82.688 % | c | 148834 | 31547 65303 | 13995 18322 556443 30.4 | 82.688 % | c | 149172 | 31547 65303 | 15395 18660 571214 30.6 | 82.688 % | c | 149678 | 31547 65303 | 16934 19166 590946 30.8 | 82.688 % | c | 150437 | 31509 65208 | 18627 19917 627694 31.5 | 82.826 % | c | 151576 | 31503 65192 | 20490 21053 676051 32.1 | 82.852 % | c | 153284 | 31462 65089 | 22539 22760 774749 34.0 | 83.010 % | c | 155846 | 31462 65089 | 24793 25322 914275 36.1 | 83.010 % | c | 159690 | 31462 65089 | 27273 29166 1077698 37.0 | 83.010 % | c | 165456 | 31450 65059 | 30000 34929 1306380 37.4 | 83.056 % | c | 174105 | 31447 65052 | 33000 43576 1753198 40.2 | 83.066 % | c | 187079 | 31420 64985 | 36300 24815 994131 40.1 | 83.168 % | c | 206540 | 31420 64985 | 39930 44276 1745057 39.4 | 83.168 % | c | 235733 | 31410 64963 | 43923 34580 1120114 32.4 | 83.199 % | c | 279522 | 31398 64933 | 48316 36368 1076415 29.6 | 83.245 % | c | 345206 | 31387 64906 | 53147 56897 1731001 30.4 | 83.286 % | c ============================================================================== c [1mFound solution: -34[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 407607 | 31371 64837 | 10457 69202 2220207 32.1 | 83.286 % | c | 407708 | 31371 64837 | 11502 21207 509732 24.0 | 83.349 % | c | 407858 | 31371 64837 | 12652 21357 514760 24.1 | 83.349 % | c | 408084 | 31371 64837 | 13918 21583 523197 24.2 | 83.349 % | c | 408421 | 31371 64837 | 15310 21920 537769 24.5 | 83.349 % | c | 408927 | 31371 64837 | 16841 22426 560502 25.0 | 83.349 % | c | 409687 | 31341 64767 | 18525 23178 592062 25.5 | 83.446 % | c | 410826 | 31341 64767 | 20377 24317 636022 26.2 | 83.446 % | c | 412534 | 31341 64767 | 22415 26025 707984 27.2 | 83.446 % | c | 415097 | 31341 64767 | 24657 28588 779097 27.3 | 83.446 % | c | 418942 | 31341 64767 | 27122 32433 897343 27.7 | 83.446 % | c | 424708 | 31341 64767 | 29835 38199 1050979 27.5 | 83.446 % | c | 433357 | 31341 64767 | 32818 46848 1391591 29.7 | 83.446 % | c | 446331 | 31332 64746 | 36100 27082 843797 31.2 | 83.476 % | c | 465792 | 31329 64739 | 39710 46542 1633843 35.1 | 83.487 % | c | 494985 | 31256 64553 | 43681 39503 1039816 26.3 | 83.767 % | c | 538775 | 31101 64220 | 48049 32061 824480 25.7 | 83.982 % | c | 604460 | 30912 63770 | 52854 25803 577004 22.4 | 84.630 % |
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/16430/stat): 16430 (minisat+_script) R 16429 16430 9854 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785279466 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/16430/statm): 174 3 169 147 0 27 0 [pid=16430] 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=16431 New process pid=16432 New process pid=16433 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=16432) exited with status: 0 One traced child (pid=16433) exited with status: 0 One traced child (pid=16431) exited with status: 0 New process pid=16434 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-frb35-17-3.opb [startup+10.0039 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 2155 0 0 0 980 9 0 0 25 0 1 0 1785279471 9764864 2142 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 2384 2142 145 145 0 2239 0 [pid=16434] vsize: 9536 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 11660 [startup+20.0057 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 2238 0 0 0 1978 10 0 0 25 0 1 0 1785279471 10104832 2225 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 2467 2225 145 145 0 2322 0 [pid=16434] vsize: 9868 Current children cumulated CPU time (s) 19.89 Current children cumulated vsize (Kb) 11992 [startup+30.0065 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 2676 0 0 0 2971 13 0 0 25 0 1 0 1785279471 11902976 2663 4294967295 134512640 135094434 3221224448 3221223072 134557616 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 2906 2663 145 145 0 2761 0 [pid=16434] vsize: 11624 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 13748 [startup+40.0073 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 3283 0 0 0 3958 17 0 0 25 0 1 0 1785279471 14426112 3270 4294967295 134512640 135094434 3221224448 3221223104 134558164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 3522 3270 145 145 0 3377 0 [pid=16434] vsize: 14088 Current children cumulated CPU time (s) 39.76 Current children cumulated vsize (Kb) 16212 [startup+50.0081 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 3776 0 0 0 4950 21 0 0 25 0 1 0 1785279471 16420864 3763 4294967295 134512640 135094434 3221224448 3221223040 134556928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 4009 3763 145 145 0 3864 0 [pid=16434] vsize: 16036 Current children cumulated CPU time (s) 49.72 Current children cumulated vsize (Kb) 18160 [startup+60.0089 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 4144 0 0 0 5942 24 0 0 25 0 1 0 1785279471 17907712 4131 4294967295 134512640 135094434 3221224448 3221223120 134556454 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 4372 4131 145 145 0 4227 0 [pid=16434] vsize: 17488 Current children cumulated CPU time (s) 59.67 Current children cumulated vsize (Kb) 19612 [startup+70.0107 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 4574 0 0 0 6935 28 0 0 25 0 1 0 1785279471 19779584 4561 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 4829 4561 145 145 0 4684 0 [pid=16434] vsize: 19316 Current children cumulated CPU time (s) 69.64 Current children cumulated vsize (Kb) 21440 [startup+80.0115 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 4942 0 0 0 7928 31 0 0 25 0 1 0 1785279471 21270528 4929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 5193 4929 145 145 0 5048 0 [pid=16434] vsize: 20772 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 22896 [startup+90.0133 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5279 0 0 0 8921 34 0 0 25 0 1 0 1785279471 22716416 5266 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 5546 5266 145 145 0 5401 0 [pid=16434] vsize: 22184 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 24308 [startup+100.014 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5279 0 0 0 9921 35 0 0 25 0 1 0 1785279471 22716416 5266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 5546 5266 145 145 0 5401 0 [pid=16434] vsize: 22184 Current children cumulated CPU time (s) 99.57 Current children cumulated vsize (Kb) 24308 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5279 0 0 0 10921 35 0 0 25 0 1 0 1785279471 22716416 5266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 5546 5266 145 145 0 5401 0 [pid=16434] vsize: 22184 Current children cumulated CPU time (s) 109.57 Current children cumulated vsize (Kb) 24308 [startup+120.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5279 0 0 0 11921 35 0 0 25 0 1 0 1785279471 22716416 5266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 5546 5266 145 145 0 5401 0 [pid=16434] vsize: 22184 Current children cumulated CPU time (s) 119.57 Current children cumulated vsize (Kb) 24308 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5387 0 0 0 12920 35 0 0 25 0 1 0 1785279471 23158784 5374 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 5654 5374 145 145 0 5509 0 [pid=16434] vsize: 22616 Current children cumulated CPU time (s) 129.56 Current children cumulated vsize (Kb) 24740 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 5777 0 0 0 13912 39 0 0 25 0 1 0 1785279471 24764416 5764 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6046 5764 145 145 0 5901 0 [pid=16434] vsize: 24184 Current children cumulated CPU time (s) 139.52 Current children cumulated vsize (Kb) 26308 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6098 0 0 0 14905 42 0 0 25 0 1 0 1785279471 26058752 6085 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6362 6085 145 145 0 6217 0 [pid=16434] vsize: 25448 Current children cumulated CPU time (s) 149.48 Current children cumulated vsize (Kb) 27572 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 15900 44 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 159.45 Current children cumulated vsize (Kb) 28472 [startup+170.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 16900 44 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221222856 134782835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 169.45 Current children cumulated vsize (Kb) 28472 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 17899 45 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 179.45 Current children cumulated vsize (Kb) 28472 [startup+190.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 18899 45 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 189.45 Current children cumulated vsize (Kb) 28472 [startup+200.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 19899 46 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 199.46 Current children cumulated vsize (Kb) 28472 [startup+210.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 20898 47 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 209.46 Current children cumulated vsize (Kb) 28472 [startup+220.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6323 0 0 0 21898 47 0 0 25 0 1 0 1785279471 26980352 6310 4294967295 134512640 135094434 3221224448 3221223104 134557962 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6587 6310 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 219.46 Current children cumulated vsize (Kb) 28472 [startup+230.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6326 0 0 0 22897 47 0 0 25 0 1 0 1785279471 26980352 6313 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6587 6313 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 229.45 Current children cumulated vsize (Kb) 28472 [startup+240.03 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6330 0 0 0 23897 48 0 0 25 0 1 0 1785279471 26980352 6317 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6587 6317 145 145 0 6442 0 [pid=16434] vsize: 26348 Current children cumulated CPU time (s) 239.46 Current children cumulated vsize (Kb) 28472 [startup+250.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 24897 48 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 249.46 Current children cumulated vsize (Kb) 28500 [startup+260.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 25897 48 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 259.46 Current children cumulated vsize (Kb) 28500 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 26897 48 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 269.46 Current children cumulated vsize (Kb) 28500 [startup+280.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 27897 48 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 279.46 Current children cumulated vsize (Kb) 28500 [startup+290.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 28897 48 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 289.46 Current children cumulated vsize (Kb) 28500 [startup+300.034 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 29896 49 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 299.46 Current children cumulated vsize (Kb) 28500 [startup+310.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 30895 49 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 309.45 Current children cumulated vsize (Kb) 28500 [startup+320.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 31895 50 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 319.46 Current children cumulated vsize (Kb) 28500 [startup+330.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 32894 50 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223040 134557328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 329.45 Current children cumulated vsize (Kb) 28500 [startup+340.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 33894 50 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 339.45 Current children cumulated vsize (Kb) 28500 [startup+350.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 34895 50 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 349.46 Current children cumulated vsize (Kb) 28500 [startup+360.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 35894 51 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 359.46 Current children cumulated vsize (Kb) 28500 [startup+370.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 36894 51 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 369.46 Current children cumulated vsize (Kb) 28500 [startup+380.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 37894 51 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 379.46 Current children cumulated vsize (Kb) 28500 [startup+390.044 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 38894 51 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 389.46 Current children cumulated vsize (Kb) 28500 [startup+400.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6338 0 0 0 39894 52 0 0 25 0 1 0 1785279471 27009024 6325 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6325 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 399.47 Current children cumulated vsize (Kb) 28500 [startup+410.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6339 0 0 0 40893 52 0 0 25 0 1 0 1785279471 27009024 6326 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6326 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 409.46 Current children cumulated vsize (Kb) 28500 [startup+420.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6339 0 0 0 41893 52 0 0 25 0 1 0 1785279471 27009024 6326 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6326 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 419.46 Current children cumulated vsize (Kb) 28500 [startup+430.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6339 0 0 0 42893 53 0 0 25 0 1 0 1785279471 27009024 6326 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6326 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 429.47 Current children cumulated vsize (Kb) 28500 [startup+440.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6339 0 0 0 43893 53 0 0 25 0 1 0 1785279471 27009024 6326 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6326 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 439.47 Current children cumulated vsize (Kb) 28500 [startup+450.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6340 0 0 0 44892 53 0 0 25 0 1 0 1785279471 27009024 6327 4294967295 134512640 135094434 3221224448 3221223104 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6327 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 449.46 Current children cumulated vsize (Kb) 28500 [startup+460.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6340 0 0 0 45892 53 0 0 25 0 1 0 1785279471 27009024 6327 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6327 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 459.46 Current children cumulated vsize (Kb) 28500 [startup+470.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6340 0 0 0 46892 54 0 0 25 0 1 0 1785279471 27009024 6327 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6327 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 469.47 Current children cumulated vsize (Kb) 28500 [startup+480.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6340 0 0 0 47892 54 0 0 25 0 1 0 1785279471 27009024 6327 4294967295 134512640 135094434 3221224448 3221223040 134556776 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6327 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 479.47 Current children cumulated vsize (Kb) 28500 [startup+490.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6340 0 0 0 48892 54 0 0 25 0 1 0 1785279471 27009024 6327 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6327 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 489.47 Current children cumulated vsize (Kb) 28500 [startup+500.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6342 0 0 0 49892 54 0 0 25 0 1 0 1785279471 27009024 6329 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6329 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 499.47 Current children cumulated vsize (Kb) 28500 [startup+510.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 50891 55 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 509.47 Current children cumulated vsize (Kb) 28500 [startup+520.061 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 51891 55 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223040 134552003 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 519.47 Current children cumulated vsize (Kb) 28500 [startup+530.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 52891 56 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 529.48 Current children cumulated vsize (Kb) 28500 [startup+540.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 53891 56 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 539.48 Current children cumulated vsize (Kb) 28500 [startup+550.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 54890 56 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 549.47 Current children cumulated vsize (Kb) 28500 [startup+560.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 55890 57 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 559.48 Current children cumulated vsize (Kb) 28500 [startup+570.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 56890 57 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 569.48 Current children cumulated vsize (Kb) 28500 [startup+580.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6343 0 0 0 57890 57 0 0 25 0 1 0 1785279471 27009024 6330 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6594 6330 145 145 0 6449 0 [pid=16434] vsize: 26376 Current children cumulated CPU time (s) 579.48 Current children cumulated vsize (Kb) 28500 [startup+590.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6363 0 0 0 58889 58 0 0 25 0 1 0 1785279471 27131904 6350 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6624 6350 145 145 0 6479 0 [pid=16434] vsize: 26496 Current children cumulated CPU time (s) 589.48 Current children cumulated vsize (Kb) 28620 [startup+600.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 59889 58 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 599.48 Current children cumulated vsize (Kb) 28876 [startup+610.071 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 60889 59 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223120 134556499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 609.49 Current children cumulated vsize (Kb) 28876 [startup+620.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 61889 59 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 619.49 Current children cumulated vsize (Kb) 28876 [startup+630.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 62889 59 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 629.49 Current children cumulated vsize (Kb) 28876 [startup+640.076 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 63888 60 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 639.49 Current children cumulated vsize (Kb) 28876 [startup+650.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 64888 60 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221222896 134782601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 649.49 Current children cumulated vsize (Kb) 28876 [startup+660.078 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 65888 60 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 659.49 Current children cumulated vsize (Kb) 28876 [startup+670.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 66889 60 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 669.5 Current children cumulated vsize (Kb) 28876 [startup+680.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 67888 60 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 679.49 Current children cumulated vsize (Kb) 28876 [startup+690.081 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6367 0 0 0 68888 61 0 0 25 0 1 0 1785279471 27394048 6354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6354 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 689.5 Current children cumulated vsize (Kb) 28876 [startup+700.082 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6369 0 0 0 69889 61 0 0 25 0 1 0 1785279471 27394048 6356 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6356 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 699.51 Current children cumulated vsize (Kb) 28876 [startup+710.083 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 70889 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 709.51 Current children cumulated vsize (Kb) 28876 [startup+720.084 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 71889 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 719.51 Current children cumulated vsize (Kb) 28876 [startup+730.085 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 72889 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 729.51 Current children cumulated vsize (Kb) 28876 [startup+740.086 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 73890 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223120 134556291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 739.52 Current children cumulated vsize (Kb) 28876 [startup+750.087 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 74890 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 749.52 Current children cumulated vsize (Kb) 28876 [startup+760.088 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 75890 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 759.52 Current children cumulated vsize (Kb) 28876 [startup+770.089 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 76890 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 769.52 Current children cumulated vsize (Kb) 28876 [startup+780.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 77890 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 779.52 Current children cumulated vsize (Kb) 28876 [startup+790.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 78891 61 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 789.53 Current children cumulated vsize (Kb) 28876 [startup+800.091 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 79890 62 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 799.53 Current children cumulated vsize (Kb) 28876 [startup+810.092 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 80890 62 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 809.53 Current children cumulated vsize (Kb) 28876 [startup+820.093 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 81888 63 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 819.52 Current children cumulated vsize (Kb) 28876 [startup+830.093 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 82888 64 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 829.53 Current children cumulated vsize (Kb) 28876 [startup+840.094 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 83888 64 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 839.53 Current children cumulated vsize (Kb) 28876 [startup+850.095 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 84888 64 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 849.53 Current children cumulated vsize (Kb) 28876 [startup+860.096 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 85888 64 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 859.53 Current children cumulated vsize (Kb) 28876 [startup+870.097 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 86888 64 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 869.53 Current children cumulated vsize (Kb) 28876 [startup+880.097 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 87888 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 879.54 Current children cumulated vsize (Kb) 28876 [startup+890.099 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 88889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 889.55 Current children cumulated vsize (Kb) 28876 [startup+900.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 89889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 899.55 Current children cumulated vsize (Kb) 28876 [startup+910.101 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 90889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 909.55 Current children cumulated vsize (Kb) 28876 [startup+920.102 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 91889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 919.55 Current children cumulated vsize (Kb) 28876 [startup+930.103 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 92889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 929.55 Current children cumulated vsize (Kb) 28876 [startup+940.104 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 93889 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 939.55 Current children cumulated vsize (Kb) 28876 [startup+950.106 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 94890 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 949.56 Current children cumulated vsize (Kb) 28876 [startup+960.106 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 95890 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 959.56 Current children cumulated vsize (Kb) 28876 [startup+970.106 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 96890 65 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 969.56 Current children cumulated vsize (Kb) 28876 [startup+980.107 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 97890 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 979.57 Current children cumulated vsize (Kb) 28876 [startup+990.108 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 98890 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 989.57 Current children cumulated vsize (Kb) 28876 [startup+1000.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 99891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 999.58 Current children cumulated vsize (Kb) 28876 [startup+1010.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 100891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1009.58 Current children cumulated vsize (Kb) 28876 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 101891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223040 134556876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1019.58 Current children cumulated vsize (Kb) 28876 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 102891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1029.58 Current children cumulated vsize (Kb) 28876 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 103891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1039.58 Current children cumulated vsize (Kb) 28876 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 104891 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1049.58 Current children cumulated vsize (Kb) 28876 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 105892 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1059.59 Current children cumulated vsize (Kb) 28876 [startup+1070.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 106892 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1069.59 Current children cumulated vsize (Kb) 28876 [startup+1080.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 107892 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1079.59 Current children cumulated vsize (Kb) 28876 [startup+1090.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 108892 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1089.59 Current children cumulated vsize (Kb) 28876 [startup+1100.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 109892 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1099.59 Current children cumulated vsize (Kb) 28876 [startup+1110.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 110893 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1109.6 Current children cumulated vsize (Kb) 28876 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 111893 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1119.6 Current children cumulated vsize (Kb) 28876 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 112893 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1129.6 Current children cumulated vsize (Kb) 28876 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 113893 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1139.6 Current children cumulated vsize (Kb) 28876 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 114893 66 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1149.6 Current children cumulated vsize (Kb) 28876 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 115893 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1159.61 Current children cumulated vsize (Kb) 28876 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 116893 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1169.61 Current children cumulated vsize (Kb) 28876 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 117894 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1179.62 Current children cumulated vsize (Kb) 28876 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 118894 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1189.62 Current children cumulated vsize (Kb) 28876 [startup+1200.13 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 119894 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1199.62 Current children cumulated vsize (Kb) 28876 [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 120894 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1209.62 Current children cumulated vsize (Kb) 28876 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 16434 Raw data (/proc/16430/stat): 16430 (minisat+_script) S 16429 16430 9854 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1785279466 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16430/statm): 531 226 485 147 0 384 0 [pid=16430] vsize: 2124 Raw data (/proc/16434/stat): 16434 (minisat+_64-bit) R 16430 16430 9854 0 -1 0 6372 0 0 0 120894 67 0 0 25 0 1 0 1785279471 27394048 6359 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16434/statm): 6688 6359 145 145 0 6543 0 [pid=16434] vsize: 26752 Current children cumulated CPU time (s) 1209.62 Current children cumulated vsize (Kb) 28876 Sending SIGTERM to -16430 Sleeping 2 seconds One traced child (pid=16430) ended because it received signal 15 (SIGTERM) One traced child (pid=16434) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1209.63 CPU user time (s): 1208.95 CPU system time (s): 0.685895 CPU usage (%): 99.9579 Max. virtual memory (cumulated for all children) (Kb): 28876
ERROR: no interpretation found !