Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-5.opb |
MD5SUM | 70070c820bc7d178cc8f33b42e0deead |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -30 |
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 | 28143 |
Number of constraints which are clauses | 28143 |
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 wulflinc28 THE 2005-09-18 18:42:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2693 boxname=wulflinc28 idbench=349 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 70070c820bc7d178cc8f33b42e0deead /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb IDLAUNCH: 2693 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 930284 kB Buffers: 33892 kB Cached: 42320 kB SwapCached: 696 kB Active: 61420 kB Inactive: 17368 kB HighTotal: 131008 kB HighFree: 85064 kB LowTotal: 903652 kB LowFree: 845220 kB SwapTotal: 2097640 kB SwapFree: 2096372 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5812 kB Slab: 19956 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:02:56 (client local time) WITH STATUS 10 IN 1209.6 SECONDS stats: 2693 7 1209.6 10
c Parsing PB file... c Converting 28143 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 | 28143 56286 | 9381 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -21[0m c ---[ 0]---> Sorter-cost:26814 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 56290 122394 | 18763 0 0 nan | 0.000 % | c | 100 | 55818 121416 | 20639 78 529 6.8 | 1.319 % | c | 250 | 55350 120416 | 22703 201 1432 7.1 | 2.831 % | c | 475 | 54323 118193 | 24973 376 3383 9.0 | 5.942 % | c ============================================================================== c [1mFound solution: -26[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 678 | 53263 115977 | 17754 507 5021 9.9 | 5.942 % | c | 778 | 52841 115047 | 19529 588 6229 10.6 | 11.045 % | c | 928 | 52322 113884 | 21482 715 7585 10.6 | 12.707 % | c | 1153 | 51428 111886 | 23630 895 9815 11.0 | 15.557 % | c | 1490 | 49468 107434 | 25993 1105 12672 11.5 | 22.140 % | c | 1996 | 47638 103232 | 28592 1527 18207 11.9 | 28.026 % | c | 2756 | 44784 96705 | 31452 2088 27733 13.3 | 37.330 % | c | 3895 | 41359 88683 | 34597 2945 40667 13.8 | 48.818 % | c ============================================================================== c [1mFound solution: -27[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4578 | 40279 86235 | 13426 3372 48651 14.4 | 48.818 % | c | 4678 | 39986 85593 | 14768 3439 49906 14.5 | 53.601 % | c | 4828 | 39929 85464 | 16245 3585 53525 14.9 | 53.786 % | c | 5053 | 39738 84989 | 17870 3769 58890 15.6 | 54.485 % | c | 5390 | 39304 83962 | 19657 3970 63529 16.0 | 55.987 % | c | 5897 | 38689 82488 | 21622 4286 73190 17.1 | 58.330 % | c | 6656 | 37185 78940 | 23784 4674 86185 18.4 | 63.301 % | c | 7795 | 36622 77561 | 26163 5675 129966 22.9 | 65.275 % | c | 9504 | 35725 75401 | 28779 7136 192067 26.9 | 68.457 % | 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 | 10440 | 35152 73982 | 11717 7917 243425 30.7 | 68.457 % | c | 10540 | 35113 73891 | 12888 7988 246532 30.9 | 70.655 % | c | 10690 | 35113 73891 | 14177 8138 257579 31.7 | 70.655 % | c | 10915 | 35077 73801 | 15595 8322 262608 31.6 | 70.789 % | c | 11252 | 34978 73564 | 17154 8601 274225 31.9 | 71.134 % | 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 | 11391 | 34971 73570 | 11657 8688 275965 31.8 | 71.134 % | c | 11491 | 34902 73413 | 12822 8759 278380 31.8 | 71.445 % | c | 11641 | 34902 73413 | 14104 8909 284047 31.9 | 71.446 % | c | 11867 | 34896 73399 | 15515 9119 294059 32.2 | 71.466 % | c | 12204 | 34763 73092 | 17067 9394 321190 34.2 | 71.903 % | c | 12711 | 34609 72711 | 18773 9712 337264 34.7 | 72.472 % | c | 13470 | 34605 72698 | 20651 10457 386838 37.0 | 72.487 % | c | 14610 | 34380 72154 | 22716 11454 436165 38.1 | 73.293 % | c | 16319 | 33765 70670 | 24987 12907 541843 42.0 | 75.434 % | 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 | 16658 | 33651 70365 | 11217 13078 538486 41.2 | 75.434 % | c | 16758 | 33651 70365 | 12338 13178 543720 41.3 | 75.826 % | c | 16908 | 33598 70240 | 13572 13315 549004 41.2 | 76.011 % | c | 17133 | 33492 69992 | 14929 13474 555912 41.3 | 76.371 % | c | 17471 | 33492 69992 | 16422 13812 572516 41.5 | 76.370 % | c | 17978 | 33390 69747 | 18065 14288 590646 41.3 | 76.730 % | c | 18737 | 33266 69453 | 19871 15005 645411 43.0 | 77.151 % | c | 19876 | 33263 69446 | 21858 16138 775398 48.0 | 77.161 % | c | 21586 | 33025 68873 | 24044 17787 883974 49.7 | 78.013 % | c | 24149 | 33025 68873 | 26449 20350 1110021 54.5 | 78.013 % | c | 27994 | 33025 68873 | 29094 24195 1446802 59.8 | 78.013 % | c | 33762 | 32912 68606 | 32003 29913 1976061 66.1 | 78.408 % | c | 42412 | 32688 68047 | 35203 38230 2602127 68.1 | 79.250 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54813 | 32709 68118 | 10903 50607 3631857 71.8 | 79.250 % | c | 54913 | 32665 68010 | 11993 17614 1027595 58.3 | 79.420 % | c | 55063 | 32665 68010 | 13192 17764 1033328 58.2 | 79.420 % | c | 55288 | 32632 67926 | 14511 17973 1042889 58.0 | 79.537 % | c | 55625 | 32632 67926 | 15963 18310 1077898 58.9 | 79.537 % | c | 56133 | 32626 67909 | 17559 18796 1115938 59.4 | 79.563 % | c | 56892 | 32626 67909 | 19315 19555 1163074 59.5 | 79.563 % | c | 58031 | 32585 67812 | 21246 20688 1247141 60.3 | 79.706 % | c | 59739 | 32585 67812 | 23371 22396 1358285 60.6 | 79.706 % | 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 | 61766 | 32459 67492 | 10819 24393 1480169 60.7 | 79.706 % | c | 61866 | 32459 67492 | 11900 24493 1483862 60.6 | 80.152 % | c | 62016 | 32422 67401 | 13090 24627 1493869 60.7 | 80.285 % | c | 62241 | 32400 67340 | 14400 24844 1515014 61.0 | 80.372 % | c | 62579 | 32361 67247 | 15840 25167 1534905 61.0 | 80.510 % | c | 63085 | 32361 67247 | 17424 25673 1569859 61.1 | 80.510 % | c | 63845 | 32361 67247 | 19166 26433 1617338 61.2 | 80.510 % | c | 64985 | 32361 67247 | 21083 27573 1724425 62.5 | 80.510 % | c | 66693 | 32361 67247 | 23191 29281 1823567 62.3 | 80.510 % | c | 69255 | 32361 67247 | 25510 31843 2022398 63.5 | 80.510 % | c | 73099 | 32266 67009 | 28061 35630 2258988 63.4 | 80.852 % | c | 78867 | 32266 67009 | 30867 41398 2541641 61.4 | 80.852 % | c | 87517 | 32261 66998 | 33954 17592 605784 34.4 | 80.868 % | c | 100493 | 32145 66707 | 37350 30555 1527180 50.0 | 81.251 % | c | 119954 | 32136 66686 | 41085 50010 2776028 55.5 | 81.282 % | c | 149146 | 32059 66501 | 45193 39406 2390640 60.7 | 81.558 % | c | 192935 | 32018 66406 | 49713 40611 2365930 58.3 | 81.696 % | 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 | 234340 | 31964 66282 | 10654 33803 1904300 56.3 | 81.696 % | c | 234440 | 31964 66282 | 11719 16070 660384 41.1 | 81.909 % | c | 234590 | 31939 66229 | 12891 16216 667281 41.1 | 81.980 % | c | 234817 | 31939 66229 | 14180 16443 680004 41.4 | 81.980 % | c | 235155 | 31853 66019 | 15598 16755 688813 41.1 | 82.286 % | c | 235661 | 31853 66019 | 17158 17261 714839 41.4 | 82.286 % | c | 236420 | 31848 66006 | 18874 18019 754497 41.9 | 82.307 % | c | 237559 | 31848 66006 | 20761 19158 827477 43.2 | 82.307 % | c | 239268 | 31848 66006 | 22837 20867 941214 45.1 | 82.307 % | c | 241830 | 31845 65999 | 25121 23424 1134066 48.4 | 82.317 % | c | 245674 | 31832 65966 | 27633 27261 1379284 50.6 | 82.368 % | c | 251442 | 31821 65939 | 30397 33025 1770495 53.6 | 82.409 % | c | 260091 | 31723 65693 | 33436 41618 2363593 56.8 | 82.781 % | c | 273065 | 31702 65642 | 36780 21888 1194237 54.6 | 82.858 % | c | 292526 | 31595 65388 | 40458 41329 2455787 59.4 | 83.236 % | c | 321718 | 31590 65375 | 44504 31574 1206245 38.2 | 83.256 % | c | 365507 | 31587 65368 | 48954 33871 1201100 35.5 | 83.266 % | c | 431191 | 31587 65368 | 53850 55118 1835677 33.3 | 83.266 % | c | 529717 | 31516 65201 | 59235 54938 1748182 31.8 | 83.511 % |
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/2176/stat): 2176 (minisat+_script) R 2175 2176 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843512947 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/2176/statm): 174 3 169 147 0 27 0 [pid=2176] 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=2177 New process pid=2178 New process pid=2179 execve syscall for /bin/sed executable One traced child (pid=2178) 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=2179) exited with status: 0 One traced child (pid=2177) exited with status: 0 New process pid=2180 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-frb35-17-5.opb [startup+10.0042 s] Raw data (loadavg): 0.93 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2157 0 0 0 981 7 0 0 25 0 1 0 1843512952 9723904 2144 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/2180/statm): 2374 2144 145 145 0 2229 0 [pid=2180] vsize: 9496 Current children cumulated CPU time (s) 9.89 Current children cumulated vsize (Kb) 11620 [startup+20.0059 s] Raw data (loadavg): 0.94 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2261 0 0 0 1979 8 0 0 25 0 1 0 1843512952 10158080 2248 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 2480 2248 145 145 0 2335 0 [pid=2180] vsize: 9920 Current children cumulated CPU time (s) 19.88 Current children cumulated vsize (Kb) 12044 [startup+30.0065 s] Raw data (loadavg): 0.95 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 2741 0 0 0 2971 11 0 0 25 0 1 0 1843512952 12124160 2728 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 2960 2728 145 145 0 2815 0 [pid=2180] vsize: 11840 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 13964 [startup+40.0072 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 3321 0 0 0 3962 15 0 0 25 0 1 0 1843512952 14536704 3308 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 3549 3308 145 145 0 3404 0 [pid=2180] vsize: 14196 Current children cumulated CPU time (s) 39.78 Current children cumulated vsize (Kb) 16320 [startup+50.0079 s] Raw data (loadavg): 0.96 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 3903 0 0 0 4951 19 0 0 19 0 1 0 1843512952 16896000 3890 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 4125 3890 145 145 0 3980 0 [pid=2180] vsize: 16500 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 18624 [startup+60.0086 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 4463 0 0 0 5942 23 0 0 25 0 1 0 1843512952 19169280 4450 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 4680 4450 145 145 0 4535 0 [pid=2180] vsize: 18720 Current children cumulated CPU time (s) 59.66 Current children cumulated vsize (Kb) 20844 [startup+70.0092 s] Raw data (loadavg): 0.97 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 4855 0 0 0 6935 26 0 0 25 0 1 0 1843512952 20885504 4842 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 5099 4842 145 145 0 4954 0 [pid=2180] vsize: 20396 Current children cumulated CPU time (s) 69.62 Current children cumulated vsize (Kb) 22520 [startup+80.0099 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 5252 0 0 0 7926 30 0 0 25 0 1 0 1843512952 22495232 5239 4294967295 134512640 135094434 3221224448 3221223040 134556904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 5492 5239 145 145 0 5347 0 [pid=2180] vsize: 21968 Current children cumulated CPU time (s) 79.57 Current children cumulated vsize (Kb) 24092 [startup+90.0106 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 5641 0 0 0 8919 33 0 0 25 0 1 0 1843512952 24072192 5628 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 5877 5628 145 145 0 5732 0 [pid=2180] vsize: 23508 Current children cumulated CPU time (s) 89.53 Current children cumulated vsize (Kb) 25632 [startup+100.011 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6053 0 0 0 9913 35 0 0 25 0 1 0 1843512952 25739264 6040 4294967295 134512640 135094434 3221224448 3221223104 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6284 6040 145 145 0 6139 0 [pid=2180] vsize: 25136 Current children cumulated CPU time (s) 99.49 Current children cumulated vsize (Kb) 27260 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6189 0 0 0 10911 36 0 0 25 0 1 0 1843512952 26292224 6176 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6419 6176 145 145 0 6274 0 [pid=2180] vsize: 25676 Current children cumulated CPU time (s) 109.48 Current children cumulated vsize (Kb) 27800 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 11911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 119.48 Current children cumulated vsize (Kb) 27956 [startup+130.013 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 12911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 129.48 Current children cumulated vsize (Kb) 27956 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 13911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223040 134557393 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 139.48 Current children cumulated vsize (Kb) 27956 [startup+150.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 14911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 149.48 Current children cumulated vsize (Kb) 27956 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 15911 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 159.48 Current children cumulated vsize (Kb) 27956 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 16912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 169.49 Current children cumulated vsize (Kb) 27956 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 17912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 179.49 Current children cumulated vsize (Kb) 27956 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 18912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 27956 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 19912 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 199.49 Current children cumulated vsize (Kb) 27956 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 20913 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 27956 [startup+220.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6209 0 0 0 21913 36 0 0 25 0 1 0 1843512952 26451968 6196 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6196 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 219.5 Current children cumulated vsize (Kb) 27956 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6210 0 0 0 22913 36 0 0 25 0 1 0 1843512952 26451968 6197 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6197 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 229.5 Current children cumulated vsize (Kb) 27956 [startup+240.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6214 0 0 0 23913 36 0 0 25 0 1 0 1843512952 26451968 6201 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6201 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 239.5 Current children cumulated vsize (Kb) 27956 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 24913 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 249.5 Current children cumulated vsize (Kb) 27956 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 25914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 259.51 Current children cumulated vsize (Kb) 27956 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 26914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 269.51 Current children cumulated vsize (Kb) 27956 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 27914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 279.51 Current children cumulated vsize (Kb) 27956 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 28914 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 289.51 Current children cumulated vsize (Kb) 27956 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 29915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 299.52 Current children cumulated vsize (Kb) 27956 [startup+310.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 30915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 309.52 Current children cumulated vsize (Kb) 27956 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6216 0 0 0 31915 36 0 0 25 0 1 0 1843512952 26451968 6203 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6458 6203 145 145 0 6313 0 [pid=2180] vsize: 25832 Current children cumulated CPU time (s) 319.52 Current children cumulated vsize (Kb) 27956 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6231 0 0 0 32915 36 0 0 25 0 1 0 1843512952 26529792 6218 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6477 6218 145 145 0 6332 0 [pid=2180] vsize: 25908 Current children cumulated CPU time (s) 329.52 Current children cumulated vsize (Kb) 28032 [startup+340.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6247 0 0 0 33915 36 0 0 25 0 1 0 1843512952 26611712 6234 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6497 6234 145 145 0 6352 0 [pid=2180] vsize: 25988 Current children cumulated CPU time (s) 339.52 Current children cumulated vsize (Kb) 28112 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6430 0 0 0 34913 37 0 0 25 0 1 0 1843512952 27373568 6417 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6683 6417 145 145 0 6538 0 [pid=2180] vsize: 26732 Current children cumulated CPU time (s) 349.51 Current children cumulated vsize (Kb) 28856 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 35911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223040 134551780 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0 [pid=2180] vsize: 27244 Current children cumulated CPU time (s) 359.5 Current children cumulated vsize (Kb) 29368 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 36911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0 [pid=2180] vsize: 27244 Current children cumulated CPU time (s) 369.5 Current children cumulated vsize (Kb) 29368 [startup+380.032 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6561 0 0 0 37911 38 0 0 25 0 1 0 1843512952 27897856 6548 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6811 6548 145 145 0 6666 0 [pid=2180] vsize: 27244 Current children cumulated CPU time (s) 379.5 Current children cumulated vsize (Kb) 29368 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6573 0 0 0 38911 38 0 0 25 0 1 0 1843512952 27963392 6560 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6827 6560 145 145 0 6682 0 [pid=2180] vsize: 27308 Current children cumulated CPU time (s) 389.5 Current children cumulated vsize (Kb) 29432 [startup+400.035 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6574 0 0 0 39912 38 0 0 25 0 1 0 1843512952 27963392 6561 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6827 6561 145 145 0 6682 0 [pid=2180] vsize: 27308 Current children cumulated CPU time (s) 399.51 Current children cumulated vsize (Kb) 29432 [startup+410.036 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6575 0 0 0 40912 38 0 0 25 0 1 0 1843512952 27963392 6562 4294967295 134512640 135094434 3221224448 3221223120 134555666 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6827 6562 145 145 0 6682 0 [pid=2180] vsize: 27308 Current children cumulated CPU time (s) 409.51 Current children cumulated vsize (Kb) 29432 [startup+420.037 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6576 0 0 0 41912 38 0 0 25 0 1 0 1843512952 27963392 6563 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 6827 6563 145 145 0 6682 0 [pid=2180] vsize: 27308 Current children cumulated CPU time (s) 419.51 Current children cumulated vsize (Kb) 29432 [startup+430.038 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 6891 0 0 0 42906 40 0 0 25 0 1 0 1843512952 29257728 6878 4294967295 134512640 135094434 3221224448 3221223120 134555260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7143 6878 145 145 0 6998 0 [pid=2180] vsize: 28572 Current children cumulated CPU time (s) 429.47 Current children cumulated vsize (Kb) 30696 [startup+440.039 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7264 0 0 0 43900 43 0 0 25 0 1 0 1843512952 30785536 7251 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7516 7251 145 145 0 7371 0 [pid=2180] vsize: 30064 Current children cumulated CPU time (s) 439.44 Current children cumulated vsize (Kb) 32188 [startup+450.04 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7559 0 0 0 44895 45 0 0 25 0 1 0 1843512952 31981568 7546 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7808 7546 145 145 0 7663 0 [pid=2180] vsize: 31232 Current children cumulated CPU time (s) 449.41 Current children cumulated vsize (Kb) 33356 [startup+460.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 45893 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 459.4 Current children cumulated vsize (Kb) 33912 [startup+470.041 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 46893 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 469.4 Current children cumulated vsize (Kb) 33912 [startup+480.042 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 47894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 479.41 Current children cumulated vsize (Kb) 33912 [startup+490.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 48894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 489.41 Current children cumulated vsize (Kb) 33912 [startup+500.043 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 49894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 499.41 Current children cumulated vsize (Kb) 33912 [startup+510.045 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 50894 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 509.41 Current children cumulated vsize (Kb) 33912 [startup+520.046 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 51895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 519.42 Current children cumulated vsize (Kb) 33912 [startup+530.047 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 52895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 529.42 Current children cumulated vsize (Kb) 33912 [startup+540.048 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 53895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 539.42 Current children cumulated vsize (Kb) 33912 [startup+550.049 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 54895 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 549.42 Current children cumulated vsize (Kb) 33912 [startup+560.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 55896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 559.43 Current children cumulated vsize (Kb) 33912 [startup+570.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 56896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 569.43 Current children cumulated vsize (Kb) 33912 [startup+580.051 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 57896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 579.43 Current children cumulated vsize (Kb) 33912 [startup+590.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 58896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 589.43 Current children cumulated vsize (Kb) 33912 [startup+600.052 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 59896 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 599.43 Current children cumulated vsize (Kb) 33912 [startup+610.054 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 60897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 609.44 Current children cumulated vsize (Kb) 33912 [startup+620.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 61897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 619.44 Current children cumulated vsize (Kb) 33912 [startup+630.055 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7636 0 0 0 62897 46 0 0 25 0 1 0 1843512952 32550912 7623 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7623 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 629.44 Current children cumulated vsize (Kb) 33912 [startup+640.056 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 63898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 639.45 Current children cumulated vsize (Kb) 33912 [startup+650.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 64898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 649.45 Current children cumulated vsize (Kb) 33912 [startup+660.057 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 65898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 659.45 Current children cumulated vsize (Kb) 33912 [startup+670.058 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 66898 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 669.45 Current children cumulated vsize (Kb) 33912 [startup+680.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 67899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 679.46 Current children cumulated vsize (Kb) 33912 [startup+690.059 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 68899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 689.46 Current children cumulated vsize (Kb) 33912 [startup+700.06 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 69899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 699.46 Current children cumulated vsize (Kb) 33912 [startup+710.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 70899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 709.46 Current children cumulated vsize (Kb) 33912 [startup+720.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7637 0 0 0 71899 46 0 0 25 0 1 0 1843512952 32550912 7624 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7624 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 719.46 Current children cumulated vsize (Kb) 33912 [startup+730.062 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 72900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 729.47 Current children cumulated vsize (Kb) 33912 [startup+740.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 73900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 739.47 Current children cumulated vsize (Kb) 33912 [startup+750.063 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 74900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 749.47 Current children cumulated vsize (Kb) 33912 [startup+760.064 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 75900 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134558184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 759.47 Current children cumulated vsize (Kb) 33912 [startup+770.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 76901 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 769.48 Current children cumulated vsize (Kb) 33912 [startup+780.065 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7638 0 0 0 77901 46 0 0 25 0 1 0 1843512952 32550912 7625 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7625 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 779.48 Current children cumulated vsize (Kb) 33912 [startup+790.066 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7640 0 0 0 78901 46 0 0 25 0 1 0 1843512952 32550912 7627 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7627 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 789.48 Current children cumulated vsize (Kb) 33912 [startup+800.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7640 0 0 0 79901 46 0 0 25 0 1 0 1843512952 32550912 7627 4294967295 134512640 135094434 3221224448 3221223100 134558036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7627 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 799.48 Current children cumulated vsize (Kb) 33912 [startup+810.067 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 80902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 809.49 Current children cumulated vsize (Kb) 33912 [startup+820.068 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 81902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 819.49 Current children cumulated vsize (Kb) 33912 [startup+830.069 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 82902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 829.49 Current children cumulated vsize (Kb) 33912 [startup+840.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 83902 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 839.49 Current children cumulated vsize (Kb) 33912 [startup+850.07 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 84903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 849.5 Current children cumulated vsize (Kb) 33912 [startup+860.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 85903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 859.5 Current children cumulated vsize (Kb) 33912 [startup+870.073 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 86903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 869.5 Current children cumulated vsize (Kb) 33912 [startup+880.072 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 87903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 879.5 Current children cumulated vsize (Kb) 33912 [startup+890.074 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7641 0 0 0 88903 46 0 0 25 0 1 0 1843512952 32550912 7628 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7628 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 889.5 Current children cumulated vsize (Kb) 33912 [startup+900.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7642 0 0 0 89903 46 0 0 25 0 1 0 1843512952 32550912 7629 4294967295 134512640 135094434 3221224448 3221223120 134556452 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7629 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 899.5 Current children cumulated vsize (Kb) 33912 [startup+910.075 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 90904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 909.51 Current children cumulated vsize (Kb) 33912 [startup+920.077 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 91904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 919.51 Current children cumulated vsize (Kb) 33912 [startup+930.078 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 92904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 929.51 Current children cumulated vsize (Kb) 33912 [startup+940.078 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 93904 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 939.51 Current children cumulated vsize (Kb) 33912 [startup+950.079 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 94905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 949.52 Current children cumulated vsize (Kb) 33912 [startup+960.079 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 95905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 959.52 Current children cumulated vsize (Kb) 33912 [startup+970.079 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 96905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 969.52 Current children cumulated vsize (Kb) 33912 [startup+980.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 97905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 979.52 Current children cumulated vsize (Kb) 33912 [startup+990.082 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 98905 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 989.52 Current children cumulated vsize (Kb) 33912 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 99906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 999.53 Current children cumulated vsize (Kb) 33912 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 100906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1009.53 Current children cumulated vsize (Kb) 33912 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 101906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1019.53 Current children cumulated vsize (Kb) 33912 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 102906 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1029.53 Current children cumulated vsize (Kb) 33912 [startup+1040.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 103907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1039.54 Current children cumulated vsize (Kb) 33912 [startup+1050.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 104907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1049.54 Current children cumulated vsize (Kb) 33912 [startup+1060.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 105907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1059.54 Current children cumulated vsize (Kb) 33912 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 106907 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1069.54 Current children cumulated vsize (Kb) 33912 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 107908 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1079.55 Current children cumulated vsize (Kb) 33912 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 108908 46 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1089.55 Current children cumulated vsize (Kb) 33912 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 109908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223136 134554739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1099.56 Current children cumulated vsize (Kb) 33912 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 110908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1109.56 Current children cumulated vsize (Kb) 33912 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7645 0 0 0 111908 47 0 0 25 0 1 0 1843512952 32550912 7632 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7632 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1119.56 Current children cumulated vsize (Kb) 33912 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7646 0 0 0 112908 47 0 0 25 0 1 0 1843512952 32550912 7633 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7633 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1129.56 Current children cumulated vsize (Kb) 33912 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7649 0 0 0 113909 47 0 0 25 0 1 0 1843512952 32550912 7636 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7636 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1139.57 Current children cumulated vsize (Kb) 33912 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 114909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1149.57 Current children cumulated vsize (Kb) 33912 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 115909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1159.57 Current children cumulated vsize (Kb) 33912 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 116909 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1169.57 Current children cumulated vsize (Kb) 33912 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 117910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1179.58 Current children cumulated vsize (Kb) 33912 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 118910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1189.58 Current children cumulated vsize (Kb) 33912 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 119910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1199.58 Current children cumulated vsize (Kb) 33912 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 120910 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1209.58 Current children cumulated vsize (Kb) 33912 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.99 2/57 2180 Raw data (/proc/2176/stat): 2176 (minisat+_script) S 2175 2176 20115 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843512947 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/2176/statm): 531 226 485 147 0 384 0 [pid=2176] vsize: 2124 Raw data (/proc/2180/stat): 2180 (minisat+_64-bit) R 2176 2176 20115 0 -1 0 7650 0 0 0 120911 47 0 0 25 0 1 0 1843512952 32550912 7637 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/2180/statm): 7947 7637 145 145 0 7802 0 [pid=2180] vsize: 31788 Current children cumulated CPU time (s) 1209.59 Current children cumulated vsize (Kb) 33912 Sending SIGTERM to -2176 Sleeping 2 seconds One traced child (pid=2176) ended because it received signal 15 (SIGTERM) One traced child (pid=2180) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.6 CPU user time (s): 1209.11 CPU system time (s): 0.485926 CPU usage (%): 99.9572 Max. virtual memory (cumulated for all children) (Kb): 33912
ERROR: no interpretation found !