Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb |
MD5SUM | e3892e1941a878802a8ccbbd36201a02 |
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 | 27842 |
Number of constraints which are clauses | 27842 |
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 wulflinc8 THE 2005-09-18 18:39:31 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2692 boxname=wulflinc8 idbench=348 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e3892e1941a878802a8ccbbd36201a02 /oldhome/oroussel/tmp/wulflinc8/normalized-frb35-17-4.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc8/normalized-frb35-17-4.opb IDLAUNCH: 2692 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 916784 kB Buffers: 34896 kB Cached: 58016 kB SwapCached: 792 kB Active: 67960 kB Inactive: 27664 kB HighTotal: 131008 kB HighFree: 69076 kB LowTotal: 903652 kB LowFree: 847708 kB SwapTotal: 2097136 kB SwapFree: 2095876 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5752 kB Slab: 16612 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 18:59:41 (client local time) WITH STATUS 10 IN 1209.68 SECONDS stats: 2692 7 1209.68 10
c Parsing PB file... c Converting 27842 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 | 27842 55684 | 9280 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56133 122130 | 18711 0 0 nan | 0.000 % | c | 100 | 55674 121173 | 20582 85 517 6.1 | 1.318 % | c | 250 | 55337 120462 | 22640 201 1671 8.3 | 2.285 % | c | 475 | 53886 117283 | 24904 355 3653 10.3 | 6.749 % | c | 813 | 52308 113815 | 27394 620 7389 11.9 | 11.632 % | c | 1319 | 49554 107621 | 30134 953 11439 12.0 | 20.509 % | c | 2078 | 46551 100685 | 33147 1523 18456 12.1 | 30.615 % | c | 3217 | 42835 92193 | 36462 2389 34261 14.3 | 42.639 % | 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 | 3273 | 42557 91588 | 14185 2416 34615 14.3 | 42.639 % | c | 3373 | 42214 90786 | 15603 2489 35595 14.3 | 45.030 % | c | 3523 | 41934 90117 | 17163 2594 37012 14.3 | 45.977 % | c | 3748 | 41522 89143 | 18880 2783 39915 14.3 | 47.372 % | c | 4086 | 40623 87001 | 20768 2975 42882 14.4 | 50.494 % | c | 4593 | 39615 84625 | 22845 3304 51715 15.7 | 53.972 % | c | 5353 | 38103 81054 | 25129 3854 65467 17.0 | 59.168 % | c | 6492 | 37040 78558 | 27642 4854 94566 19.5 | 62.852 % | 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 | 7236 | 36536 77417 | 12178 5459 115634 21.2 | 62.852 % | c | 7336 | 36373 77022 | 13395 5525 117833 21.3 | 65.194 % | c | 7486 | 36245 76711 | 14735 5659 121848 21.5 | 65.636 % | c | 7712 | 35618 75194 | 16208 5758 121613 21.1 | 67.804 % | c | 8049 | 35083 73909 | 17829 5937 129670 21.8 | 69.674 % | c | 8555 | 35082 73906 | 19612 6440 149607 23.2 | 69.679 % | c | 9314 | 34665 72910 | 21574 7108 172599 24.3 | 71.138 % | c | 10454 | 34563 72672 | 23731 8226 223484 27.2 | 71.487 % | c | 12162 | 34403 72291 | 26104 9826 305581 31.1 | 72.052 % | c | 14725 | 33512 70136 | 28715 11797 413482 35.0 | 75.269 % | c | 18569 | 32730 68273 | 31586 14907 673193 45.2 | 78.002 % | c | 24336 | 32584 67918 | 34745 20503 1088479 53.1 | 78.521 % | 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 | 25008 | 32376 67375 | 10792 20807 1127008 54.2 | 78.521 % | c | 25109 | 32333 67266 | 11871 20854 1131597 54.3 | 79.396 % | c | 25259 | 32266 67098 | 13058 20933 1134331 54.2 | 79.653 % | c | 25484 | 32266 67098 | 14364 21158 1153914 54.5 | 79.653 % | c | 25824 | 32266 67098 | 15800 21498 1181497 55.0 | 79.653 % | 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 | 26069 | 32269 67111 | 10756 20959 1109301 52.9 | 79.653 % | c | 26169 | 32220 66999 | 11831 21035 1113907 53.0 | 79.898 % | c | 26319 | 32220 66999 | 13014 21185 1119388 52.8 | 79.898 % | c | 26544 | 32174 66891 | 14316 21380 1132489 53.0 | 80.051 % | c | 26881 | 32174 66891 | 15747 21717 1150097 53.0 | 80.051 % | c | 27388 | 32126 66770 | 17322 22203 1170894 52.7 | 80.215 % | c | 28148 | 32036 66557 | 19054 22829 1208152 52.9 | 80.527 % | c | 29287 | 32036 66557 | 20960 23968 1254726 52.4 | 80.527 % | c | 30995 | 32008 66487 | 23056 25554 1358136 53.1 | 80.634 % | c | 33557 | 32008 66487 | 25362 28116 1511958 53.8 | 80.634 % | c | 37401 | 32008 66487 | 27898 31960 1790963 56.0 | 80.634 % | c | 43167 | 31963 66380 | 30688 37641 2179278 57.9 | 80.788 % | c | 51816 | 31942 66327 | 33756 46095 2740539 59.5 | 80.865 % | c | 64790 | 31936 66313 | 37132 23972 1287927 53.7 | 80.885 % | 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 | 83994 | 31772 65908 | 10590 43119 2704132 62.7 | 80.885 % | c | 84094 | 31769 65901 | 11649 16788 764343 45.5 | 81.544 % | c | 84245 | 31761 65883 | 12813 16934 773077 45.7 | 81.569 % | c | 84470 | 31761 65883 | 14095 17159 787038 45.9 | 81.569 % | c | 84807 | 31629 65553 | 15504 17469 799984 45.8 | 82.070 % | c | 85314 | 31616 65520 | 17055 17970 827588 46.1 | 82.121 % | c | 86073 | 31535 65323 | 18760 18695 873445 46.7 | 82.407 % | c | 87212 | 31529 65309 | 20636 19831 940958 47.4 | 82.428 % | c | 88920 | 31523 65295 | 22700 21535 1039370 48.3 | 82.448 % | c | 91482 | 31523 65295 | 24970 24097 1198465 49.7 | 82.448 % | c | 95326 | 31486 65206 | 27467 27922 1432420 51.3 | 82.581 % | c | 101092 | 31447 65117 | 30214 33656 1817647 54.0 | 82.708 % | c | 109742 | 31438 65094 | 33235 42294 2206478 52.2 | 82.744 % | c | 122717 | 31429 65073 | 36559 23198 776943 33.5 | 82.775 % | c | 142179 | 31427 65069 | 40215 42658 1545047 36.2 | 82.780 % | c | 171371 | 31424 65062 | 44237 32274 1209176 37.5 | 82.790 % | c | 215161 | 31396 64996 | 48660 32992 1383853 41.9 | 82.887 % | c | 280846 | 31348 64880 | 53526 51753 1853976 35.8 | 83.061 % | c | 379372 | 31268 64690 | 58879 48632 1483738 30.5 | 83.337 % | 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 | 387520 | 31254 64622 | 10418 56778 1800142 31.7 | 83.337 % | c | 387621 | 31254 64622 | 11459 21874 574796 26.3 | 83.395 % | c | 387771 | 31254 64622 | 12605 22024 579120 26.3 | 83.395 % | c | 387996 | 31254 64622 | 13866 22249 585284 26.3 | 83.395 % | c | 388334 | 31254 64622 | 15252 22587 595104 26.3 | 83.395 % | c | 388840 | 31254 64622 | 16778 23093 611433 26.5 | 83.395 % | c | 389599 | 31254 64622 | 18456 23852 651357 27.3 | 83.395 % | c | 390738 | 31254 64622 | 20301 24991 708484 28.3 | 83.395 % | c | 392446 | 31254 64622 | 22331 26699 784774 29.4 | 83.395 % | c | 395008 | 31254 64622 | 24565 29261 882101 30.1 | 83.395 % | c | 398852 | 31254 64622 | 27021 33105 1025751 31.0 | 83.395 % | c | 404619 | 31237 64583 | 29723 38861 1224818 31.5 | 83.451 % | c | 413269 | 31193 64477 | 32696 19145 554379 29.0 | 83.609 % | c | 426243 | 31188 64466 | 35965 32115 1008537 31.4 | 83.625 % | c | 445704 | 31188 64466 | 39562 51576 1732486 33.6 | 83.624 % | c | 474896 | 31175 64437 | 43518 43794 1320198 30.1 | 83.665 % | c | 518685 | 31066 64153 | 47870 45690 1182298 25.9 | 84.089 % | c ============================================================================== c [1mFound solution: -35[0m c ---[ 0]---> Sorter-cost:23198 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 565168 | 49180 106489 | 16393 38187 1077494 28.2 | 84.089 % | c | 565268 | 49180 106489 | 18032 15309 289280 18.9 | 55.800 % | c | 565418 | 49180 106489 | 19835 15459 294371 19.0 | 55.800 % | c | 565643 | 49180 106489 | 21819 15684 302669 19.3 | 55.800 % | c | 565980 | 49180 106489 | 24000 16021 312388 19.5 | 55.800 % | c | 566490 | 49180 106489 | 26401 16531 329375 19.9 | 55.800 % | c | 567250 | 49180 106489 | 29041 17291 353999 20.5 | 55.800 % | c | 568389 | 49180 106489 | 31945 18430 386682 21.0 | 55.800 % | c | 570097 | 49180 106489 | 35139 20138 435618 21.6 | 55.800 % | c | 572659 | 49180 106489 | 38653 22700 507140 22.3 | 55.800 % | c | 576504 | 49139 106407 | 42519 26544 621579 23.4 | 55.877 % | c | 582270 | 49139 106407 | 46771 32310 777211 24.1 | 55.877 % | c | 590919 | 49102 106333 | 51448 40958 1110939 27.1 | 55.940 % | c | 603893 | 49102 106333 | 56593 53932 1518995 28.2 | 55.940 % |
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/7283/stat): 7283 (minisat+_script) R 7282 7283 27660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1771690102 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/7283/statm): 174 3 169 147 0 27 0 [pid=7283] 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=7284 New process pid=7285 New process pid=7286 execve syscall for /bin/sed executable One traced child (pid=7285) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=7286) exited with status: 0 One traced child (pid=7284) exited with status: 0 New process pid=7287 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc8/normalized-frb35-17-4.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.95 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2089 0 0 0 982 7 0 0 25 0 1 0 1771690107 9388032 2076 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 2292 2076 145 145 0 2147 0 [pid=7287] vsize: 9168 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 11292 [startup+20.0051 s] Raw data (loadavg): 0.94 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2235 0 0 0 1980 8 0 0 25 0 1 0 1771690107 10084352 2222 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 2462 2222 145 145 0 2317 0 [pid=7287] vsize: 9848 Current children cumulated CPU time (s) 19.89 Current children cumulated vsize (Kb) 11972 [startup+30.0059 s] Raw data (loadavg): 0.95 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 2748 0 0 0 2970 12 0 0 25 0 1 0 1771690107 12189696 2735 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 2976 2735 145 145 0 2831 0 [pid=7287] vsize: 11904 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 14028 [startup+40.0067 s] Raw data (loadavg): 0.95 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 3300 0 0 0 3960 17 0 0 25 0 1 0 1771690107 14495744 3287 4294967295 134512640 135094434 3221224448 3221223040 134557238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 3539 3287 145 145 0 3394 0 [pid=7287] vsize: 14156 Current children cumulated CPU time (s) 39.78 Current children cumulated vsize (Kb) 16280 [startup+50.0075 s] Raw data (loadavg): 0.96 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 3619 0 0 0 4954 19 0 0 25 0 1 0 1771690107 15785984 3606 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 3854 3606 145 145 0 3709 0 [pid=7287] vsize: 15416 Current children cumulated CPU time (s) 49.74 Current children cumulated vsize (Kb) 17540 [startup+60.0093 s] Raw data (loadavg): 0.97 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4072 0 0 0 5946 23 0 0 25 0 1 0 1771690107 17616896 4059 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 4301 4059 145 145 0 4156 0 [pid=7287] vsize: 17204 Current children cumulated CPU time (s) 59.7 Current children cumulated vsize (Kb) 19328 [startup+70.01 s] Raw data (loadavg): 0.97 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4510 0 0 0 6937 26 0 0 25 0 1 0 1771690107 19521536 4497 4294967295 134512640 135094434 3221224448 3221223104 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 4766 4497 145 145 0 4621 0 [pid=7287] vsize: 19064 Current children cumulated CPU time (s) 69.64 Current children cumulated vsize (Kb) 21188 [startup+80.0108 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 4895 0 0 0 7929 30 0 0 25 0 1 0 1771690107 21078016 4882 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5146 4882 145 145 0 5001 0 [pid=7287] vsize: 20584 Current children cumulated CPU time (s) 79.6 Current children cumulated vsize (Kb) 22708 [startup+90.0116 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5211 0 0 0 8922 33 0 0 25 0 1 0 1771690107 22355968 5198 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5458 5198 145 145 0 5313 0 [pid=7287] vsize: 21832 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 23956 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5504 0 0 0 9915 36 0 0 25 0 1 0 1771690107 23539712 5491 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5747 5491 145 145 0 5602 0 [pid=7287] vsize: 22988 Current children cumulated CPU time (s) 99.52 Current children cumulated vsize (Kb) 25112 [startup+110.014 s] Raw data (loadavg): 0.98 0.96 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 10913 37 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0 [pid=7287] vsize: 23596 Current children cumulated CPU time (s) 109.51 Current children cumulated vsize (Kb) 25720 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 11912 37 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0 [pid=7287] vsize: 23596 Current children cumulated CPU time (s) 119.5 Current children cumulated vsize (Kb) 25720 [startup+130.016 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 12912 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223040 134557518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0 [pid=7287] vsize: 23596 Current children cumulated CPU time (s) 129.51 Current children cumulated vsize (Kb) 25720 [startup+140.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 13911 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0 [pid=7287] vsize: 23596 Current children cumulated CPU time (s) 139.5 Current children cumulated vsize (Kb) 25720 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5658 0 0 0 14911 38 0 0 25 0 1 0 1771690107 24162304 5645 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5899 5645 145 145 0 5754 0 [pid=7287] vsize: 23596 Current children cumulated CPU time (s) 149.5 Current children cumulated vsize (Kb) 25720 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 15911 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 159.5 Current children cumulated vsize (Kb) 25876 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 16912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 169.51 Current children cumulated vsize (Kb) 25876 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 17912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 179.51 Current children cumulated vsize (Kb) 25876 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 18912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 189.51 Current children cumulated vsize (Kb) 25876 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 19912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 199.51 Current children cumulated vsize (Kb) 25876 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 20912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 209.51 Current children cumulated vsize (Kb) 25876 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 21912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 219.51 Current children cumulated vsize (Kb) 25876 [startup+230.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 22912 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 229.51 Current children cumulated vsize (Kb) 25876 [startup+240.022 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 23913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 239.52 Current children cumulated vsize (Kb) 25876 [startup+250.023 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 24913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 249.52 Current children cumulated vsize (Kb) 25876 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 25913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 259.52 Current children cumulated vsize (Kb) 25876 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5678 0 0 0 26913 38 0 0 25 0 1 0 1771690107 24322048 5665 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5665 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 269.52 Current children cumulated vsize (Kb) 25876 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5680 0 0 0 27913 38 0 0 25 0 1 0 1771690107 24322048 5667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5667 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 279.52 Current children cumulated vsize (Kb) 25876 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 28914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 289.53 Current children cumulated vsize (Kb) 25876 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 29914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 299.53 Current children cumulated vsize (Kb) 25876 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 30914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 309.53 Current children cumulated vsize (Kb) 25876 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 31914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223120 134556239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 319.53 Current children cumulated vsize (Kb) 25876 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 32914 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 329.53 Current children cumulated vsize (Kb) 25876 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 33915 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 339.54 Current children cumulated vsize (Kb) 25876 [startup+350.027 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 34915 38 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 349.54 Current children cumulated vsize (Kb) 25876 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 35915 39 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 359.55 Current children cumulated vsize (Kb) 25876 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5684 0 0 0 36915 39 0 0 25 0 1 0 1771690107 24322048 5671 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5671 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 25876 [startup+380.029 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 37915 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 379.55 Current children cumulated vsize (Kb) 25876 [startup+390.03 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 38916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 389.56 Current children cumulated vsize (Kb) 25876 [startup+400.03 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 39916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 399.56 Current children cumulated vsize (Kb) 25876 [startup+410.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 40916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 409.56 Current children cumulated vsize (Kb) 25876 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 41916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223040 134557175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 419.56 Current children cumulated vsize (Kb) 25876 [startup+430.031 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 42916 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 429.56 Current children cumulated vsize (Kb) 25876 [startup+440.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 43917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 439.57 Current children cumulated vsize (Kb) 25876 [startup+450.032 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 44917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 449.57 Current children cumulated vsize (Kb) 25876 [startup+460.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5688 0 0 0 45917 39 0 0 25 0 1 0 1771690107 24322048 5675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 5938 5675 145 145 0 5793 0 [pid=7287] vsize: 23752 Current children cumulated CPU time (s) 459.57 Current children cumulated vsize (Kb) 25876 [startup+470.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5804 0 0 0 46914 40 0 0 25 0 1 0 1771690107 24793088 5791 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6053 5791 145 145 0 5908 0 [pid=7287] vsize: 24212 Current children cumulated CPU time (s) 469.55 Current children cumulated vsize (Kb) 26336 [startup+480.033 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 47912 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0 [pid=7287] vsize: 24920 Current children cumulated CPU time (s) 479.54 Current children cumulated vsize (Kb) 27044 [startup+490.034 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 48913 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0 [pid=7287] vsize: 24920 Current children cumulated CPU time (s) 489.55 Current children cumulated vsize (Kb) 27044 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5919 0 0 0 49913 41 0 0 25 0 1 0 1771690107 25518080 5906 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6230 5906 145 145 0 6085 0 [pid=7287] vsize: 24920 Current children cumulated CPU time (s) 499.55 Current children cumulated vsize (Kb) 27044 [startup+510.035 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5937 0 0 0 50913 41 0 0 25 0 1 0 1771690107 25616384 5924 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6254 5924 145 145 0 6109 0 [pid=7287] vsize: 25016 Current children cumulated CPU time (s) 509.55 Current children cumulated vsize (Kb) 27140 [startup+520.036 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5944 0 0 0 51913 41 0 0 25 0 1 0 1771690107 25649152 5931 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6262 5931 145 145 0 6117 0 [pid=7287] vsize: 25048 Current children cumulated CPU time (s) 519.55 Current children cumulated vsize (Kb) 27172 [startup+530.037 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5954 0 0 0 52913 41 0 0 25 0 1 0 1771690107 25714688 5941 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6278 5941 145 145 0 6133 0 [pid=7287] vsize: 25112 Current children cumulated CPU time (s) 529.55 Current children cumulated vsize (Kb) 27236 [startup+540.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5971 0 0 0 53914 41 0 0 25 0 1 0 1771690107 25780224 5958 4294967295 134512640 135094434 3221224448 3221223120 134555940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6294 5958 145 145 0 6149 0 [pid=7287] vsize: 25176 Current children cumulated CPU time (s) 539.56 Current children cumulated vsize (Kb) 27300 [startup+550.038 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5973 0 0 0 54914 41 0 0 25 0 1 0 1771690107 25780224 5960 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6294 5960 145 145 0 6149 0 [pid=7287] vsize: 25176 Current children cumulated CPU time (s) 549.56 Current children cumulated vsize (Kb) 27300 [startup+560.039 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5986 0 0 0 55912 41 0 0 25 0 1 0 1771690107 25845760 5973 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 6310 5973 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 559.54 Current children cumulated vsize (Kb) 27364 [startup+570.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5987 0 0 0 56911 42 0 0 25 0 1 0 1771690107 25845760 5974 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5974 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 569.54 Current children cumulated vsize (Kb) 27364 [startup+580.04 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5987 0 0 0 57911 42 0 0 25 0 1 0 1771690107 25845760 5974 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5974 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 579.54 Current children cumulated vsize (Kb) 27364 [startup+590.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5989 0 0 0 58912 42 0 0 25 0 1 0 1771690107 25845760 5976 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5976 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 589.55 Current children cumulated vsize (Kb) 27364 [startup+600.042 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5993 0 0 0 59912 42 0 0 25 0 1 0 1771690107 25845760 5980 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5980 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 599.55 Current children cumulated vsize (Kb) 27364 [startup+610.043 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 60912 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 609.55 Current children cumulated vsize (Kb) 27364 [startup+620.044 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 61912 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 619.55 Current children cumulated vsize (Kb) 27364 [startup+630.044 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 62913 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 629.56 Current children cumulated vsize (Kb) 27364 [startup+640.045 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 5994 0 0 0 63913 42 0 0 25 0 1 0 1771690107 25845760 5981 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6310 5981 145 145 0 6165 0 [pid=7287] vsize: 25240 Current children cumulated CPU time (s) 639.56 Current children cumulated vsize (Kb) 27364 [startup+650.045 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6012 0 0 0 64913 42 0 0 25 0 1 0 1771690107 25944064 5999 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6334 5999 145 145 0 6189 0 [pid=7287] vsize: 25336 Current children cumulated CPU time (s) 649.56 Current children cumulated vsize (Kb) 27460 [startup+660.046 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6035 0 0 0 65913 42 0 0 25 0 1 0 1771690107 26071040 6022 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6022 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 659.56 Current children cumulated vsize (Kb) 27584 [startup+670.047 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6037 0 0 0 66913 42 0 0 25 0 1 0 1771690107 26071040 6024 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6024 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 669.56 Current children cumulated vsize (Kb) 27584 [startup+680.048 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6038 0 0 0 67914 42 0 0 25 0 1 0 1771690107 26071040 6025 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6025 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 679.57 Current children cumulated vsize (Kb) 27584 [startup+690.048 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6038 0 0 0 68914 42 0 0 25 0 1 0 1771690107 26071040 6025 4294967295 134512640 135094434 3221224448 3221223040 134557152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6025 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 689.57 Current children cumulated vsize (Kb) 27584 [startup+700.048 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6040 0 0 0 69914 42 0 0 25 0 1 0 1771690107 26071040 6027 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6027 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 699.57 Current children cumulated vsize (Kb) 27584 [startup+710.049 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6041 0 0 0 70914 42 0 0 25 0 1 0 1771690107 26071040 6028 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6028 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 709.57 Current children cumulated vsize (Kb) 27584 [startup+720.05 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 71915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 719.58 Current children cumulated vsize (Kb) 27584 [startup+730.051 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 72915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 729.58 Current children cumulated vsize (Kb) 27584 [startup+740.051 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 73915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 739.58 Current children cumulated vsize (Kb) 27584 [startup+750.051 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 74915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 749.58 Current children cumulated vsize (Kb) 27584 [startup+760.052 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 75915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134558017 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 759.58 Current children cumulated vsize (Kb) 27584 [startup+770.053 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 76916 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 769.59 Current children cumulated vsize (Kb) 27584 [startup+780.054 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6042 0 0 0 77915 42 0 0 25 0 1 0 1771690107 26071040 6029 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6365 6029 145 145 0 6220 0 [pid=7287] vsize: 25460 Current children cumulated CPU time (s) 779.58 Current children cumulated vsize (Kb) 27584 [startup+790.054 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6053 0 0 0 78915 42 0 0 25 0 1 0 1771690107 26136576 6040 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6040 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 789.58 Current children cumulated vsize (Kb) 27648 [startup+800.055 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 79916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 799.59 Current children cumulated vsize (Kb) 27648 [startup+810.056 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 80916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 809.59 Current children cumulated vsize (Kb) 27648 [startup+820.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 81916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 819.59 Current children cumulated vsize (Kb) 27648 [startup+830.057 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 82916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 829.59 Current children cumulated vsize (Kb) 27648 [startup+840.058 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 83916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 839.59 Current children cumulated vsize (Kb) 27648 [startup+850.058 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 84916 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 849.59 Current children cumulated vsize (Kb) 27648 [startup+860.059 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 85917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 859.6 Current children cumulated vsize (Kb) 27648 [startup+870.06 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 86917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223120 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 869.6 Current children cumulated vsize (Kb) 27648 [startup+880.059 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 87917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 879.6 Current children cumulated vsize (Kb) 27648 [startup+890.06 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 88917 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223072 134557653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 889.6 Current children cumulated vsize (Kb) 27648 [startup+900.061 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 89918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 899.61 Current children cumulated vsize (Kb) 27648 [startup+910.062 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 90918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 909.61 Current children cumulated vsize (Kb) 27648 [startup+920.062 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 91918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 919.61 Current children cumulated vsize (Kb) 27648 [startup+930.063 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6054 0 0 0 92918 42 0 0 25 0 1 0 1771690107 26136576 6041 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6381 6041 145 145 0 6236 0 [pid=7287] vsize: 25524 Current children cumulated CPU time (s) 929.61 Current children cumulated vsize (Kb) 27648 [startup+940.064 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6064 0 0 0 93918 42 0 0 25 0 1 0 1771690107 26202112 6051 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6051 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 939.61 Current children cumulated vsize (Kb) 27712 [startup+950.064 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 94919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 949.62 Current children cumulated vsize (Kb) 27712 [startup+960.065 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 95919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 959.62 Current children cumulated vsize (Kb) 27712 [startup+970.065 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 96919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 969.62 Current children cumulated vsize (Kb) 27712 [startup+980.066 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 97919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 979.62 Current children cumulated vsize (Kb) 27712 [startup+990.067 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 98919 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 989.62 Current children cumulated vsize (Kb) 27712 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 99920 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 999.63 Current children cumulated vsize (Kb) 27712 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6065 0 0 0 100920 42 0 0 25 0 1 0 1771690107 26202112 6052 4294967295 134512640 135094434 3221224448 3221222992 134562149 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6397 6052 145 145 0 6252 0 [pid=7287] vsize: 25588 Current children cumulated CPU time (s) 1009.63 Current children cumulated vsize (Kb) 27712 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6078 0 0 0 101920 43 0 0 25 0 1 0 1771690107 26267648 6065 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6065 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1019.64 Current children cumulated vsize (Kb) 27776 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 102920 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1029.64 Current children cumulated vsize (Kb) 27776 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 103921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1039.65 Current children cumulated vsize (Kb) 27776 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 104921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1049.65 Current children cumulated vsize (Kb) 27776 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 105921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1059.65 Current children cumulated vsize (Kb) 27776 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 106921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1069.65 Current children cumulated vsize (Kb) 27776 [startup+1080.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 107921 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1079.65 Current children cumulated vsize (Kb) 27776 [startup+1090.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 108922 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1089.66 Current children cumulated vsize (Kb) 27776 [startup+1100.07 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6081 0 0 0 109920 43 0 0 25 0 1 0 1771690107 26267648 6068 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/7287/statm): 6413 6068 145 145 0 6268 0 [pid=7287] vsize: 25652 Current children cumulated CPU time (s) 1099.64 Current children cumulated vsize (Kb) 27776 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 110918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558208 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1109.64 Current children cumulated vsize (Kb) 31252 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 111918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1119.64 Current children cumulated vsize (Kb) 31252 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 112918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1129.64 Current children cumulated vsize (Kb) 31252 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 113918 45 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1139.64 Current children cumulated vsize (Kb) 31252 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 114919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1149.66 Current children cumulated vsize (Kb) 31252 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 115919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1159.66 Current children cumulated vsize (Kb) 31252 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 116919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1169.66 Current children cumulated vsize (Kb) 31252 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 117919 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1179.66 Current children cumulated vsize (Kb) 31252 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 118920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1189.67 Current children cumulated vsize (Kb) 31252 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 119920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1199.67 Current children cumulated vsize (Kb) 31252 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 120920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1209.67 Current children cumulated vsize (Kb) 31252 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.97 2/57 7287 Raw data (/proc/7283/stat): 7283 (minisat+_script) S 7282 7283 27660 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1771690102 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/7283/statm): 531 226 485 147 0 384 0 [pid=7283] vsize: 2124 Raw data (/proc/7287/stat): 7287 (minisat+_64-bit) R 7283 7283 27660 0 -1 0 6738 0 0 0 120920 46 0 0 25 0 1 0 1771690107 29827072 6713 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/7287/statm): 7282 6713 145 145 0 7137 0 [pid=7287] vsize: 29128 Current children cumulated CPU time (s) 1209.67 Current children cumulated vsize (Kb) 31252 Sending SIGTERM to -7283 Sleeping 2 seconds One traced child (pid=7283) ended because it received signal 15 (SIGTERM) One traced child (pid=7287) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.1 CPU time (s): 1209.68 CPU user time (s): 1209.21 CPU system time (s): 0.474927 CPU usage (%): 99.9655 Max. virtual memory (cumulated for all children) (Kb): 31252
ERROR: no interpretation found !