Name | submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-9symml.opb |
MD5SUM | 48809ba02390b1184dab90aed89aff8e |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4517 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 651 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 28138 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 28138 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 281.067 |
Number of variables | 651 |
Total number of constraints | 1658 |
Number of constraints which are clauses | 1656 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 2 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42 |
LAUNCH ON wulflinc18 THE 2005-09-18 18:10:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2590 boxname=wulflinc18 idbench=246 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 48809ba02390b1184dab90aed89aff8e /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb IDLAUNCH: 2590 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 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: 916828 kB Buffers: 35288 kB Cached: 47984 kB SwapCached: 844 kB Active: 66240 kB Inactive: 19660 kB HighTotal: 131008 kB HighFree: 80136 kB LowTotal: 903652 kB LowFree: 836692 kB SwapTotal: 2097892 kB SwapFree: 2096548 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 26400 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:30:21 (client local time) WITH STATUS 10 IN 1208.03 SECONDS stats: 2590 7 1208.03 10
c Parsing PB file... c Converting 1579 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 | 1552 6592 | 517 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 6227[0m c ---[ 0]---> Sorter-cost:101537 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 240640 564833 | 80213 0 0 nan | 0.000 % | c | 100 | 240294 564068 | 88234 97 554 5.7 | 0.124 % | c | 250 | 239475 562211 | 97057 242 1239 5.1 | 0.372 % | c | 475 | 239475 562211 | 106763 467 2772 5.9 | 0.372 % | c | 812 | 239475 562211 | 117439 804 5080 6.3 | 0.372 % | c | 1318 | 239344 561924 | 129183 1306 10185 7.8 | 0.418 % | c | 2077 | 239154 561493 | 142102 2061 21860 10.6 | 0.491 % | c | 3217 | 238924 560969 | 156312 3195 43126 13.5 | 0.574 % | c | 4925 | 238870 560853 | 171943 4898 147580 30.1 | 0.598 % | c | 7488 | 238545 560119 | 189138 7447 199936 26.8 | 0.694 % | c | 11333 | 238182 559291 | 208051 11252 264258 23.5 | 0.811 % | c | 17099 | 237688 558162 | 228857 16994 352844 20.8 | 0.969 % | c | 25751 | 237623 558014 | 251742 25643 903840 35.2 | 0.991 % | c ============================================================================== c [1mFound solution: 5682[0m c ---[ 0]---> Sorter-cost:81756 Base: 2 5 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29821 | 435689 1020432 | 145229 29713 1042028 35.1 | 0.991 % | c | 29922 | 435689 1020432 | 159751 29814 1042915 35.0 | 0.570 % | c | 30072 | 435689 1020432 | 175727 29964 1043798 34.8 | 0.570 % | c | 30297 | 435410 1019814 | 193299 30186 1047211 34.7 | 0.617 % | c | 30635 | 434343 1017394 | 212629 30492 1053024 34.5 | 0.811 % | c | 31141 | 434343 1017394 | 233892 30998 1066445 34.4 | 0.811 % | c | 31900 | 434343 1017394 | 257282 31757 1076013 33.9 | 0.811 % | c | 33039 | 434343 1017394 | 283010 32896 1253111 38.1 | 0.811 % | c | 34748 | 434343 1017394 | 311311 34605 1301864 37.6 | 0.811 % | c | 37311 | 434331 1017367 | 342442 37166 1344836 36.2 | 0.813 % | c | 41155 | 434331 1017367 | 376686 41010 1457843 35.5 | 0.813 % | c | 46922 | 434331 1017367 | 414355 46777 2162173 46.2 | 0.813 % | c | 55572 | 434242 1017165 | 455790 55424 3473368 62.7 | 0.830 % | c | 68546 | 434242 1017165 | 501369 68398 6520599 95.3 | 0.830 % | c | 88008 | 434235 1017150 | 551506 87857 9667702 110.0 | 0.832 % | c | 117200 | 433771 1016104 | 606657 117042 19603779 167.5 | 0.911 % |
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/5246/stat): 5246 (minisat+_script) R 5245 5246 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843273101 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5246/statm): 174 3 169 147 0 27 0 [pid=5246] 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=5247 New process pid=5248 New process pid=5249 execve syscall for /bin/sed executable One traced child (pid=5248) 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=5249) exited with status: 0 One traced child (pid=5247) exited with status: 0 New process pid=5250 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-9symml.opb [startup+10.0039 s] Raw data (loadavg): 0.91 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 7894 0 0 0 935 29 0 0 25 0 1 0 1843273106 33902592 7443 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 8277 7443 145 145 0 8132 0 [pid=5250] vsize: 33108 Current children cumulated CPU time (s) 9.65 Current children cumulated vsize (Kb) 35232 [startup+20.0058 s] Raw data (loadavg): 0.92 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8018 0 0 0 1934 30 0 0 25 0 1 0 1843273106 34418688 7567 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 8403 7567 145 145 0 8258 0 [pid=5250] vsize: 33612 Current children cumulated CPU time (s) 19.65 Current children cumulated vsize (Kb) 35736 [startup+30.0077 s] Raw data (loadavg): 0.93 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8106 0 0 0 2932 31 0 0 25 0 1 0 1843273106 34758656 7655 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 8486 7655 145 145 0 8341 0 [pid=5250] vsize: 33944 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 36068 [startup+40.0086 s] Raw data (loadavg): 0.94 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8194 0 0 0 3930 32 0 0 25 0 1 0 1843273106 35131392 7743 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 8577 7743 145 145 0 8432 0 [pid=5250] vsize: 34308 Current children cumulated CPU time (s) 39.63 Current children cumulated vsize (Kb) 36432 [startup+50.0095 s] Raw data (loadavg): 0.95 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8331 0 0 0 4928 33 0 0 25 0 1 0 1843273106 35667968 7880 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 8708 7880 145 145 0 8563 0 [pid=5250] vsize: 34832 Current children cumulated CPU time (s) 49.62 Current children cumulated vsize (Kb) 36956 [startup+60.0105 s] Raw data (loadavg): 0.96 0.94 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8571 0 0 0 5925 34 0 0 25 0 1 0 1843273106 36663296 8120 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 8951 8120 145 145 0 8806 0 [pid=5250] vsize: 35804 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 37928 [startup+70.0114 s] Raw data (loadavg): 0.96 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8770 0 0 0 6922 36 0 0 25 0 1 0 1843273106 37470208 8319 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 9148 8319 145 145 0 9003 0 [pid=5250] vsize: 36592 Current children cumulated CPU time (s) 69.59 Current children cumulated vsize (Kb) 38716 [startup+80.0133 s] Raw data (loadavg): 0.97 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8862 0 0 0 7919 37 0 0 25 0 1 0 1843273106 37838848 8411 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 9238 8411 145 145 0 9093 0 [pid=5250] vsize: 36952 Current children cumulated CPU time (s) 79.57 Current children cumulated vsize (Kb) 39076 [startup+90.0142 s] Raw data (loadavg): 0.97 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 8968 0 0 0 8917 38 0 0 25 0 1 0 1843273106 38264832 8517 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 9342 8517 145 145 0 9197 0 [pid=5250] vsize: 37368 Current children cumulated CPU time (s) 89.56 Current children cumulated vsize (Kb) 39492 [startup+100.015 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 9098 0 0 0 9914 40 0 0 25 0 1 0 1843273106 38785024 8647 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 9469 8647 145 145 0 9324 0 [pid=5250] vsize: 37876 Current children cumulated CPU time (s) 99.55 Current children cumulated vsize (Kb) 40000 [startup+110.017 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15468 0 0 0 10867 65 0 0 25 0 1 0 1843273106 68468736 14562 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 16716 14562 145 145 0 16571 0 [pid=5250] vsize: 66864 Current children cumulated CPU time (s) 109.33 Current children cumulated vsize (Kb) 68988 [startup+120.019 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15529 0 0 0 11866 65 0 0 25 0 1 0 1843273106 68616192 14623 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 16752 14623 145 145 0 16607 0 [pid=5250] vsize: 67008 Current children cumulated CPU time (s) 119.32 Current children cumulated vsize (Kb) 69132 [startup+130.02 s] Raw data (loadavg): 0.98 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15661 0 0 0 12863 67 0 0 25 0 1 0 1843273106 69152768 14755 4294967295 134512640 135094434 3221224448 3221223072 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 16883 14755 145 145 0 16738 0 [pid=5250] vsize: 67532 Current children cumulated CPU time (s) 129.31 Current children cumulated vsize (Kb) 69656 [startup+140.021 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15773 0 0 0 13861 68 0 0 25 0 1 0 1843273106 69718016 14867 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17021 14867 145 145 0 16876 0 [pid=5250] vsize: 68084 Current children cumulated CPU time (s) 139.3 Current children cumulated vsize (Kb) 70208 [startup+150.022 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15829 0 0 0 14860 69 0 0 25 0 1 0 1843273106 69894144 14923 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17064 14923 145 145 0 16919 0 [pid=5250] vsize: 68256 Current children cumulated CPU time (s) 149.3 Current children cumulated vsize (Kb) 70380 [startup+160.024 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15896 0 0 0 15859 69 0 0 25 0 1 0 1843273106 70160384 14990 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17129 14990 145 145 0 16984 0 [pid=5250] vsize: 68516 Current children cumulated CPU time (s) 159.29 Current children cumulated vsize (Kb) 70640 [startup+170.025 s] Raw data (loadavg): 0.99 0.95 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 15962 0 0 0 16858 70 0 0 25 0 1 0 1843273106 70422528 15056 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17193 15056 145 145 0 17048 0 [pid=5250] vsize: 68772 Current children cumulated CPU time (s) 169.29 Current children cumulated vsize (Kb) 70896 [startup+180.027 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16024 0 0 0 17856 71 0 0 25 0 1 0 1843273106 70668288 15118 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17253 15118 145 145 0 17108 0 [pid=5250] vsize: 69012 Current children cumulated CPU time (s) 179.28 Current children cumulated vsize (Kb) 71136 [startup+190.029 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16100 0 0 0 18854 72 0 0 25 0 1 0 1843273106 70987776 15194 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17331 15194 145 145 0 17186 0 [pid=5250] vsize: 69324 Current children cumulated CPU time (s) 189.27 Current children cumulated vsize (Kb) 71448 [startup+200.029 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16209 0 0 0 19852 73 0 0 25 0 1 0 1843273106 71430144 15303 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17439 15303 145 145 0 17294 0 [pid=5250] vsize: 69756 Current children cumulated CPU time (s) 199.26 Current children cumulated vsize (Kb) 71880 [startup+210.031 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16354 0 0 0 20849 74 0 0 25 0 1 0 1843273106 72019968 15448 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17583 15448 145 145 0 17438 0 [pid=5250] vsize: 70332 Current children cumulated CPU time (s) 209.24 Current children cumulated vsize (Kb) 72456 [startup+220.032 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16484 0 0 0 21847 76 0 0 25 0 1 0 1843273106 72548352 15578 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17712 15578 145 145 0 17567 0 [pid=5250] vsize: 70848 Current children cumulated CPU time (s) 219.24 Current children cumulated vsize (Kb) 72972 [startup+230.034 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16576 0 0 0 22845 77 0 0 25 0 1 0 1843273106 72925184 15670 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17804 15670 145 145 0 17659 0 [pid=5250] vsize: 71216 Current children cumulated CPU time (s) 229.23 Current children cumulated vsize (Kb) 73340 [startup+240.035 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16742 0 0 0 23842 79 0 0 25 0 1 0 1843273106 73601024 15836 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 17969 15836 145 145 0 17824 0 [pid=5250] vsize: 71876 Current children cumulated CPU time (s) 239.22 Current children cumulated vsize (Kb) 74000 [startup+250.036 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16820 0 0 0 24841 79 0 0 25 0 1 0 1843273106 73912320 15914 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18045 15914 145 145 0 17900 0 [pid=5250] vsize: 72180 Current children cumulated CPU time (s) 249.21 Current children cumulated vsize (Kb) 74304 [startup+260.038 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16908 0 0 0 25838 80 0 0 25 0 1 0 1843273106 74268672 16002 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18132 16002 145 145 0 17987 0 [pid=5250] vsize: 72528 Current children cumulated CPU time (s) 259.19 Current children cumulated vsize (Kb) 74652 [startup+270.039 s] Raw data (loadavg): 0.99 0.96 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 16979 0 0 0 26837 82 0 0 25 0 1 0 1843273106 74555392 16073 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18202 16073 145 145 0 18057 0 [pid=5250] vsize: 72808 Current children cumulated CPU time (s) 269.2 Current children cumulated vsize (Kb) 74932 [startup+280.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17102 0 0 0 27835 83 0 0 25 0 1 0 1843273106 75059200 16196 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18325 16196 145 145 0 18180 0 [pid=5250] vsize: 73300 Current children cumulated CPU time (s) 279.19 Current children cumulated vsize (Kb) 75424 [startup+290.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17214 0 0 0 28832 85 0 0 25 0 1 0 1843273106 75513856 16308 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18436 16308 145 145 0 18291 0 [pid=5250] vsize: 73744 Current children cumulated CPU time (s) 289.18 Current children cumulated vsize (Kb) 75868 [startup+300.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17385 0 0 0 29830 86 0 0 25 0 1 0 1843273106 76206080 16479 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18605 16479 145 145 0 18460 0 [pid=5250] vsize: 74420 Current children cumulated CPU time (s) 299.17 Current children cumulated vsize (Kb) 76544 [startup+310.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17580 0 0 0 30827 88 0 0 25 0 1 0 1843273106 77000704 16674 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18799 16674 145 145 0 18654 0 [pid=5250] vsize: 75196 Current children cumulated CPU time (s) 309.16 Current children cumulated vsize (Kb) 77320 [startup+320.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17727 0 0 0 31824 89 0 0 25 0 1 0 1843273106 77598720 16821 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 18945 16821 145 145 0 18800 0 [pid=5250] vsize: 75780 Current children cumulated CPU time (s) 319.14 Current children cumulated vsize (Kb) 77904 [startup+330.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17844 0 0 0 32822 90 0 0 25 0 1 0 1843273106 78077952 16938 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19062 16938 145 145 0 18917 0 [pid=5250] vsize: 76248 Current children cumulated CPU time (s) 329.13 Current children cumulated vsize (Kb) 78372 [startup+340.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 17967 0 0 0 33819 91 0 0 25 0 1 0 1843273106 78577664 17061 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19184 17061 145 145 0 19039 0 [pid=5250] vsize: 76736 Current children cumulated CPU time (s) 339.11 Current children cumulated vsize (Kb) 78860 [startup+350.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18134 0 0 0 34817 93 0 0 25 0 1 0 1843273106 79257600 17228 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19350 17228 145 145 0 19205 0 [pid=5250] vsize: 77400 Current children cumulated CPU time (s) 349.11 Current children cumulated vsize (Kb) 79524 [startup+360.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18181 0 0 0 35816 94 0 0 25 0 1 0 1843273106 79441920 17275 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19395 17275 145 145 0 19250 0 [pid=5250] vsize: 77580 Current children cumulated CPU time (s) 359.11 Current children cumulated vsize (Kb) 79704 [startup+370.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18229 0 0 0 36814 95 0 0 25 0 1 0 1843273106 79634432 17323 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19442 17323 145 145 0 19297 0 [pid=5250] vsize: 77768 Current children cumulated CPU time (s) 369.1 Current children cumulated vsize (Kb) 79892 [startup+380.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18271 0 0 0 37813 96 0 0 25 0 1 0 1843273106 79806464 17365 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19484 17365 145 145 0 19339 0 [pid=5250] vsize: 77936 Current children cumulated CPU time (s) 379.1 Current children cumulated vsize (Kb) 80060 [startup+390.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18323 0 0 0 38812 97 0 0 25 0 1 0 1843273106 80015360 17417 4294967295 134512640 135094434 3221224448 3221223100 134562036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19535 17417 145 145 0 19390 0 [pid=5250] vsize: 78140 Current children cumulated CPU time (s) 389.1 Current children cumulated vsize (Kb) 80264 [startup+400.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18370 0 0 0 39810 97 0 0 25 0 1 0 1843273106 80207872 17464 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19582 17464 145 145 0 19437 0 [pid=5250] vsize: 78328 Current children cumulated CPU time (s) 399.08 Current children cumulated vsize (Kb) 80452 [startup+410.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18422 0 0 0 40809 98 0 0 25 0 1 0 1843273106 80416768 17516 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19633 17516 145 145 0 19488 0 [pid=5250] vsize: 78532 Current children cumulated CPU time (s) 409.08 Current children cumulated vsize (Kb) 80656 [startup+420.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18498 0 0 0 41807 99 0 0 25 0 1 0 1843273106 80728064 17592 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19709 17592 145 145 0 19564 0 [pid=5250] vsize: 78836 Current children cumulated CPU time (s) 419.07 Current children cumulated vsize (Kb) 80960 [startup+430.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18613 0 0 0 42804 101 0 0 25 0 1 0 1843273106 81195008 17707 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 19823 17707 145 145 0 19678 0 [pid=5250] vsize: 79292 Current children cumulated CPU time (s) 429.06 Current children cumulated vsize (Kb) 81416 [startup+440.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 18973 0 0 0 43798 104 0 0 25 0 1 0 1843273106 82665472 18067 4294967295 134512640 135094434 3221224448 3221223040 134551922 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 20182 18067 145 145 0 20037 0 [pid=5250] vsize: 80728 Current children cumulated CPU time (s) 439.03 Current children cumulated vsize (Kb) 82852 [startup+450.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 19378 0 0 0 44791 107 0 0 25 0 1 0 1843273106 84316160 18472 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 20585 18472 145 145 0 20440 0 [pid=5250] vsize: 82340 Current children cumulated CPU time (s) 448.99 Current children cumulated vsize (Kb) 84464 [startup+460.065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 19819 0 0 0 45786 109 0 0 25 0 1 0 1843273106 86118400 18913 4294967295 134512640 135094434 3221224448 3221223040 134557143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 21025 18913 145 145 0 20880 0 [pid=5250] vsize: 84100 Current children cumulated CPU time (s) 458.96 Current children cumulated vsize (Kb) 86224 [startup+470.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 20332 0 0 0 46781 111 0 0 25 0 1 0 1843273106 88219648 19426 4294967295 134512640 135094434 3221224448 3221223040 134557391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 21538 19426 145 145 0 21393 0 [pid=5250] vsize: 86152 Current children cumulated CPU time (s) 468.93 Current children cumulated vsize (Kb) 88276 [startup+480.068 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 20764 0 0 0 47776 113 0 0 25 0 1 0 1843273106 90247168 19858 4294967295 134512640 135094434 3221224448 3221223040 134557389 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 22033 19858 145 145 0 21888 0 [pid=5250] vsize: 88132 Current children cumulated CPU time (s) 478.9 Current children cumulated vsize (Kb) 90256 [startup+490.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21166 0 0 0 48771 116 0 0 25 0 1 0 1843273106 91897856 20260 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 22436 20260 145 145 0 22291 0 [pid=5250] vsize: 89744 Current children cumulated CPU time (s) 488.88 Current children cumulated vsize (Kb) 91868 [startup+500.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21239 0 0 0 49769 117 0 0 25 0 1 0 1843273106 92184576 20333 4294967295 134512640 135094434 3221224448 3221223136 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 22506 20333 145 145 0 22361 0 [pid=5250] vsize: 90024 Current children cumulated CPU time (s) 498.87 Current children cumulated vsize (Kb) 92148 [startup+510.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21321 0 0 0 50767 118 0 0 25 0 1 0 1843273106 92508160 20415 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 22585 20415 145 145 0 22440 0 [pid=5250] vsize: 90340 Current children cumulated CPU time (s) 508.86 Current children cumulated vsize (Kb) 92464 [startup+520.074 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21386 0 0 0 51765 119 0 0 25 0 1 0 1843273106 92770304 20480 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 22649 20480 145 145 0 22504 0 [pid=5250] vsize: 90596 Current children cumulated CPU time (s) 518.85 Current children cumulated vsize (Kb) 92720 [startup+530.076 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21530 0 0 0 52763 121 0 0 25 0 1 0 1843273106 93356032 20624 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 22792 20624 145 145 0 22647 0 [pid=5250] vsize: 91168 Current children cumulated CPU time (s) 528.85 Current children cumulated vsize (Kb) 93292 [startup+540.077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 21769 0 0 0 53760 122 0 0 25 0 1 0 1843273106 94326784 20863 4294967295 134512640 135094434 3221224448 3221223040 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 23029 20863 145 145 0 22884 0 [pid=5250] vsize: 92116 Current children cumulated CPU time (s) 538.83 Current children cumulated vsize (Kb) 94240 [startup+550.078 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22013 0 0 0 54758 123 0 0 25 0 1 0 1843273106 95322112 21107 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 23272 21107 145 145 0 23127 0 [pid=5250] vsize: 93088 Current children cumulated CPU time (s) 548.82 Current children cumulated vsize (Kb) 95212 [startup+560.079 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22271 0 0 0 55755 125 0 0 25 0 1 0 1843273106 96374784 21365 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 23529 21365 145 145 0 23384 0 [pid=5250] vsize: 94116 Current children cumulated CPU time (s) 558.81 Current children cumulated vsize (Kb) 96240 [startup+570.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22556 0 0 0 56750 127 0 0 25 0 1 0 1843273106 97542144 21650 4294967295 134512640 135094434 3221224448 3221223040 134557391 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 23814 21650 145 145 0 23669 0 [pid=5250] vsize: 95256 Current children cumulated CPU time (s) 568.78 Current children cumulated vsize (Kb) 97380 [startup+580.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 22806 0 0 0 57748 128 0 0 25 0 1 0 1843273106 98549760 21900 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 24060 21900 145 145 0 23915 0 [pid=5250] vsize: 96240 Current children cumulated CPU time (s) 578.77 Current children cumulated vsize (Kb) 98364 [startup+590.081 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23066 0 0 0 58743 130 0 0 25 0 1 0 1843273106 99672064 22160 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 24334 22160 145 145 0 24189 0 [pid=5250] vsize: 97336 Current children cumulated CPU time (s) 588.74 Current children cumulated vsize (Kb) 99460 [startup+600.082 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23302 0 0 0 59741 131 0 0 25 0 1 0 1843273106 100634624 22396 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 24569 22396 145 145 0 24424 0 [pid=5250] vsize: 98276 Current children cumulated CPU time (s) 598.73 Current children cumulated vsize (Kb) 100400 [startup+610.083 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23542 0 0 0 60738 132 0 0 25 0 1 0 1843273106 101617664 22636 4294967295 134512640 135094434 3221224448 3221223040 134556789 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 24809 22636 145 145 0 24664 0 [pid=5250] vsize: 99236 Current children cumulated CPU time (s) 608.71 Current children cumulated vsize (Kb) 101360 [startup+620.084 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23749 0 0 0 61735 134 0 0 25 0 1 0 1843273106 102461440 22843 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25015 22843 145 145 0 24870 0 [pid=5250] vsize: 100060 Current children cumulated CPU time (s) 618.7 Current children cumulated vsize (Kb) 102184 [startup+630.086 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 23966 0 0 0 62732 136 0 0 25 0 1 0 1843273106 103346176 23060 4294967295 134512640 135094434 3221224448 3221223040 134556823 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25231 23060 145 145 0 25086 0 [pid=5250] vsize: 100924 Current children cumulated CPU time (s) 628.69 Current children cumulated vsize (Kb) 103048 [startup+640.087 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24196 0 0 0 63728 137 0 0 25 0 1 0 1843273106 104288256 23290 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5250/statm): 25461 23290 145 145 0 25316 0 [pid=5250] vsize: 101844 Current children cumulated CPU time (s) 638.66 Current children cumulated vsize (Kb) 103968 [startup+650.088 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24354 0 0 0 64726 137 0 0 25 0 1 0 1843273106 104931328 23448 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25618 23448 145 145 0 25473 0 [pid=5250] vsize: 102472 Current children cumulated CPU time (s) 648.64 Current children cumulated vsize (Kb) 104596 [startup+660.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24489 0 0 0 65723 139 0 0 25 0 1 0 1843273106 105467904 23583 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25749 23583 145 145 0 25604 0 [pid=5250] vsize: 102996 Current children cumulated CPU time (s) 658.63 Current children cumulated vsize (Kb) 105120 [startup+670.091 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24626 0 0 0 66720 140 0 0 25 0 1 0 1843273106 106020864 23720 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25884 23720 145 145 0 25739 0 [pid=5250] vsize: 103536 Current children cumulated CPU time (s) 668.61 Current children cumulated vsize (Kb) 105660 [startup+680.093 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24675 0 0 0 67720 141 0 0 25 0 1 0 1843273106 106217472 23769 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25932 23769 145 145 0 25787 0 [pid=5250] vsize: 103728 Current children cumulated CPU time (s) 678.62 Current children cumulated vsize (Kb) 105852 [startup+690.094 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24742 0 0 0 68718 142 0 0 25 0 1 0 1843273106 106487808 23836 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 25998 23836 145 145 0 25853 0 [pid=5250] vsize: 103992 Current children cumulated CPU time (s) 688.61 Current children cumulated vsize (Kb) 106116 [startup+700.095 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24865 0 0 0 69717 142 0 0 25 0 1 0 1843273106 106991616 23959 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26121 23959 145 145 0 25976 0 [pid=5250] vsize: 104484 Current children cumulated CPU time (s) 698.6 Current children cumulated vsize (Kb) 106608 [startup+710.096 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 24963 0 0 0 70716 143 0 0 25 0 1 0 1843273106 107388928 24057 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26218 24057 145 145 0 26073 0 [pid=5250] vsize: 104872 Current children cumulated CPU time (s) 708.6 Current children cumulated vsize (Kb) 106996 [startup+720.096 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25074 0 0 0 71714 144 0 0 25 0 1 0 1843273106 107843584 24168 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26329 24168 145 145 0 26184 0 [pid=5250] vsize: 105316 Current children cumulated CPU time (s) 718.59 Current children cumulated vsize (Kb) 107440 [startup+730.097 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25166 0 0 0 72713 144 0 0 25 0 1 0 1843273106 108220416 24260 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26421 24260 145 145 0 26276 0 [pid=5250] vsize: 105684 Current children cumulated CPU time (s) 728.58 Current children cumulated vsize (Kb) 107808 [startup+740.098 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25290 0 0 0 73712 145 0 0 25 0 1 0 1843273106 108724224 24384 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26544 24384 145 145 0 26399 0 [pid=5250] vsize: 106176 Current children cumulated CPU time (s) 738.58 Current children cumulated vsize (Kb) 108300 [startup+750.099 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25445 0 0 0 74710 146 0 0 25 0 1 0 1843273106 109359104 24539 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26699 24539 145 145 0 26554 0 [pid=5250] vsize: 106796 Current children cumulated CPU time (s) 748.57 Current children cumulated vsize (Kb) 108920 [startup+760.1 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25612 0 0 0 75707 147 0 0 25 0 1 0 1843273106 110043136 24706 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 26866 24706 145 145 0 26721 0 [pid=5250] vsize: 107464 Current children cumulated CPU time (s) 758.55 Current children cumulated vsize (Kb) 109588 [startup+770.101 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 25826 0 0 0 76704 148 0 0 25 0 1 0 1843273106 110923776 24920 4294967295 134512640 135094434 3221224448 3221223104 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27081 24920 145 145 0 26936 0 [pid=5250] vsize: 108324 Current children cumulated CPU time (s) 768.53 Current children cumulated vsize (Kb) 110448 [startup+780.103 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26033 0 0 0 77701 150 0 0 25 0 1 0 1843273106 111763456 25127 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27286 25127 145 145 0 27141 0 [pid=5250] vsize: 109144 Current children cumulated CPU time (s) 778.52 Current children cumulated vsize (Kb) 111268 [startup+790.104 s] Raw data (loadavg): 0.99 0.97 0.96 3/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26213 0 0 0 78698 151 0 0 25 0 1 0 1843273106 112496640 25307 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27465 25307 145 145 0 27320 0 [pid=5250] vsize: 109860 Current children cumulated CPU time (s) 788.5 Current children cumulated vsize (Kb) 111984 [startup+800.104 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26378 0 0 0 79696 152 0 0 25 0 1 0 1843273106 113172480 25472 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27630 25472 145 145 0 27485 0 [pid=5250] vsize: 110520 Current children cumulated CPU time (s) 798.49 Current children cumulated vsize (Kb) 112644 [startup+810.105 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26506 0 0 0 80694 153 0 0 25 0 1 0 1843273106 113692672 25600 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27757 25600 145 145 0 27612 0 [pid=5250] vsize: 111028 Current children cumulated CPU time (s) 808.48 Current children cumulated vsize (Kb) 113152 [startup+820.106 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26685 0 0 0 81691 154 0 0 25 0 1 0 1843273106 114425856 25779 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 27936 25779 145 145 0 27791 0 [pid=5250] vsize: 111744 Current children cumulated CPU time (s) 818.46 Current children cumulated vsize (Kb) 113868 [startup+830.107 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 26829 0 0 0 82689 155 0 0 25 0 1 0 1843273106 115011584 25923 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28079 25923 145 145 0 27934 0 [pid=5250] vsize: 112316 Current children cumulated CPU time (s) 828.45 Current children cumulated vsize (Kb) 114440 [startup+840.107 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27009 0 0 0 83686 156 0 0 25 0 1 0 1843273106 115748864 26103 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28259 26103 145 145 0 28114 0 [pid=5250] vsize: 113036 Current children cumulated CPU time (s) 838.43 Current children cumulated vsize (Kb) 115160 [startup+850.108 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27161 0 0 0 84684 156 0 0 25 0 1 0 1843273106 116371456 26255 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28411 26255 145 145 0 28266 0 [pid=5250] vsize: 113644 Current children cumulated CPU time (s) 848.41 Current children cumulated vsize (Kb) 115768 [startup+860.109 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27287 0 0 0 85683 157 0 0 25 0 1 0 1843273106 116883456 26381 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28536 26381 145 145 0 28391 0 [pid=5250] vsize: 114144 Current children cumulated CPU time (s) 858.41 Current children cumulated vsize (Kb) 116268 [startup+870.11 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27445 0 0 0 86681 158 0 0 25 0 1 0 1843273106 117530624 26539 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28694 26539 145 145 0 28549 0 [pid=5250] vsize: 114776 Current children cumulated CPU time (s) 868.4 Current children cumulated vsize (Kb) 116900 [startup+880.111 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27623 0 0 0 87679 159 0 0 25 0 1 0 1843273106 118263808 26717 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 28873 26718 145 145 0 28728 0 [pid=5250] vsize: 115492 Current children cumulated CPU time (s) 878.39 Current children cumulated vsize (Kb) 117616 [startup+890.112 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27797 0 0 0 88677 160 0 0 25 0 1 0 1843273106 118968320 26891 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29045 26891 145 145 0 28900 0 [pid=5250] vsize: 116180 Current children cumulated CPU time (s) 888.38 Current children cumulated vsize (Kb) 118304 [startup+900.113 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 27974 0 0 0 89675 161 0 0 25 0 1 0 1843273106 119693312 27068 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29222 27068 145 145 0 29077 0 [pid=5250] vsize: 116888 Current children cumulated CPU time (s) 898.37 Current children cumulated vsize (Kb) 119012 [startup+910.114 s] Raw data (loadavg): 0.99 0.97 0.96 3/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28116 0 0 0 90673 161 0 0 25 0 1 0 1843273106 120270848 27210 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29363 27210 145 145 0 29218 0 [pid=5250] vsize: 117452 Current children cumulated CPU time (s) 908.35 Current children cumulated vsize (Kb) 119576 [startup+920.115 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28299 0 0 0 91671 162 0 0 25 0 1 0 1843273106 121028608 27393 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29548 27393 145 145 0 29403 0 [pid=5250] vsize: 118192 Current children cumulated CPU time (s) 918.34 Current children cumulated vsize (Kb) 120316 [startup+930.116 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28449 0 0 0 92668 164 0 0 25 0 1 0 1843273106 121630720 27543 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29695 27543 145 145 0 29550 0 [pid=5250] vsize: 118780 Current children cumulated CPU time (s) 928.33 Current children cumulated vsize (Kb) 120904 [startup+940.117 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28632 0 0 0 93666 165 0 0 25 0 1 0 1843273106 122380288 27726 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 29878 27726 145 145 0 29733 0 [pid=5250] vsize: 119512 Current children cumulated CPU time (s) 938.32 Current children cumulated vsize (Kb) 121636 [startup+950.117 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28792 0 0 0 94664 166 0 0 25 0 1 0 1843273106 123047936 27886 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30041 27886 145 145 0 29896 0 [pid=5250] vsize: 120164 Current children cumulated CPU time (s) 948.31 Current children cumulated vsize (Kb) 122288 [startup+960.119 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 28995 0 0 0 95660 168 0 0 25 0 1 0 1843273106 123871232 28089 4294967295 134512640 135094434 3221224448 3221223040 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30242 28089 145 145 0 30097 0 [pid=5250] vsize: 120968 Current children cumulated CPU time (s) 958.29 Current children cumulated vsize (Kb) 123092 [startup+970.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29151 0 0 0 96657 169 0 0 25 0 1 0 1843273106 124518400 28245 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30400 28245 145 145 0 30255 0 [pid=5250] vsize: 121600 Current children cumulated CPU time (s) 968.27 Current children cumulated vsize (Kb) 123724 [startup+980.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29275 0 0 0 97655 170 0 0 25 0 1 0 1843273106 125022208 28369 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30523 28369 145 145 0 30378 0 [pid=5250] vsize: 122092 Current children cumulated CPU time (s) 978.26 Current children cumulated vsize (Kb) 124216 [startup+990.121 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29389 0 0 0 98653 171 0 0 25 0 1 0 1843273106 125485056 28483 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30636 28483 145 145 0 30491 0 [pid=5250] vsize: 122544 Current children cumulated CPU time (s) 988.25 Current children cumulated vsize (Kb) 124668 [startup+1000.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29538 0 0 0 99650 173 0 0 25 0 1 0 1843273106 126091264 28632 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30784 28632 145 145 0 30639 0 [pid=5250] vsize: 123136 Current children cumulated CPU time (s) 998.24 Current children cumulated vsize (Kb) 125260 [startup+1010.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29679 0 0 0 100648 174 0 0 25 0 1 0 1843273106 126668800 28773 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 30925 28773 145 145 0 30780 0 [pid=5250] vsize: 123700 Current children cumulated CPU time (s) 1008.23 Current children cumulated vsize (Kb) 125824 [startup+1020.12 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29821 0 0 0 101645 175 0 0 25 0 1 0 1843273106 127250432 28915 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31067 28915 145 145 0 30922 0 [pid=5250] vsize: 124268 Current children cumulated CPU time (s) 1018.21 Current children cumulated vsize (Kb) 126392 [startup+1030.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 29971 0 0 0 102643 177 0 0 25 0 1 0 1843273106 127868928 29065 4294967295 134512640 135094434 3221224448 3221223104 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31218 29065 145 145 0 31073 0 [pid=5250] vsize: 124872 Current children cumulated CPU time (s) 1028.21 Current children cumulated vsize (Kb) 126996 [startup+1040.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30134 0 0 0 103641 178 0 0 25 0 1 0 1843273106 128532480 29228 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31380 29228 145 145 0 31235 0 [pid=5250] vsize: 125520 Current children cumulated CPU time (s) 1038.2 Current children cumulated vsize (Kb) 127644 [startup+1050.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30280 0 0 0 104639 179 0 0 25 0 1 0 1843273106 129130496 29374 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31526 29374 145 145 0 31381 0 [pid=5250] vsize: 126104 Current children cumulated CPU time (s) 1048.19 Current children cumulated vsize (Kb) 128228 [startup+1060.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30487 0 0 0 105635 180 0 0 25 0 1 0 1843273106 129974272 29581 4294967295 134512640 135094434 3221224448 3221223120 134555673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31732 29581 145 145 0 31587 0 [pid=5250] vsize: 126928 Current children cumulated CPU time (s) 1058.16 Current children cumulated vsize (Kb) 129052 [startup+1070.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30587 0 0 0 106634 181 0 0 25 0 1 0 1843273106 130383872 29681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31832 29681 145 145 0 31687 0 [pid=5250] vsize: 127328 Current children cumulated CPU time (s) 1068.16 Current children cumulated vsize (Kb) 129452 [startup+1080.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30630 0 0 0 107633 181 0 0 25 0 1 0 1843273106 130555904 29724 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 31874 29724 145 145 0 31729 0 [pid=5250] vsize: 127496 Current children cumulated CPU time (s) 1078.15 Current children cumulated vsize (Kb) 129620 [startup+1090.13 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 30872 0 0 0 108631 183 0 0 25 0 1 0 1843273106 131522560 29966 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 32110 29966 145 145 0 31965 0 [pid=5250] vsize: 128440 Current children cumulated CPU time (s) 1088.15 Current children cumulated vsize (Kb) 130564 [startup+1100.14 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31212 0 0 0 109627 185 0 0 25 0 1 0 1843273106 132915200 30306 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 32450 30306 145 145 0 32305 0 [pid=5250] vsize: 129800 Current children cumulated CPU time (s) 1098.13 Current children cumulated vsize (Kb) 131924 [startup+1110.14 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31530 0 0 0 110624 186 0 0 25 0 1 0 1843273106 134213632 30624 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 32767 30624 145 145 0 32622 0 [pid=5250] vsize: 131068 Current children cumulated CPU time (s) 1108.11 Current children cumulated vsize (Kb) 133192 [startup+1120.15 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 31911 0 0 0 111621 188 0 0 25 0 1 0 1843273106 135770112 31005 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 33147 31005 145 145 0 33002 0 [pid=5250] vsize: 132588 Current children cumulated CPU time (s) 1118.1 Current children cumulated vsize (Kb) 134712 [startup+1130.15 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 32204 0 0 0 112617 189 0 0 25 0 1 0 1843273106 136970240 31298 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 33440 31298 145 145 0 33295 0 [pid=5250] vsize: 133760 Current children cumulated CPU time (s) 1128.07 Current children cumulated vsize (Kb) 135884 [startup+1140.15 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 32600 0 0 0 113613 191 0 0 25 0 1 0 1843273106 138588160 31694 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 33835 31694 145 145 0 33690 0 [pid=5250] vsize: 135340 Current children cumulated CPU time (s) 1138.05 Current children cumulated vsize (Kb) 137464 [startup+1150.15 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33002 0 0 0 114610 193 0 0 25 0 1 0 1843273106 140234752 32096 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 34237 32096 145 145 0 34092 0 [pid=5250] vsize: 136948 Current children cumulated CPU time (s) 1148.04 Current children cumulated vsize (Kb) 139072 [startup+1160.15 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33310 0 0 0 115607 195 0 0 25 0 1 0 1843273106 141492224 32404 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 34544 32404 145 145 0 34399 0 [pid=5250] vsize: 138176 Current children cumulated CPU time (s) 1158.03 Current children cumulated vsize (Kb) 140300 [startup+1170.15 s] Raw data (loadavg): 1.07 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33700 0 0 0 116603 197 0 0 25 0 1 0 1843273106 143089664 32794 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 34934 32794 145 145 0 34789 0 [pid=5250] vsize: 139736 Current children cumulated CPU time (s) 1168.01 Current children cumulated vsize (Kb) 141860 [startup+1180.15 s] Raw data (loadavg): 1.06 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 33985 0 0 0 117600 198 0 0 25 0 1 0 1843273106 144236544 33079 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 35214 33079 145 145 0 35069 0 [pid=5250] vsize: 140856 Current children cumulated CPU time (s) 1177.99 Current children cumulated vsize (Kb) 142980 [startup+1190.15 s] Raw data (loadavg): 1.05 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34359 0 0 0 118596 200 0 0 25 0 1 0 1843273106 145764352 33453 4294967295 134512640 135094434 3221224448 3221223104 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 35587 33453 145 145 0 35442 0 [pid=5250] vsize: 142348 Current children cumulated CPU time (s) 1187.97 Current children cumulated vsize (Kb) 144472 [startup+1200.15 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34563 0 0 0 119594 201 0 0 25 0 1 0 1843273106 146595840 33657 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 35790 33657 145 145 0 35645 0 [pid=5250] vsize: 143160 Current children cumulated CPU time (s) 1197.96 Current children cumulated vsize (Kb) 145284 [startup+1210.15 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34581 0 0 0 120594 201 0 0 25 0 1 0 1843273106 146665472 33675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 35807 33675 145 145 0 35662 0 [pid=5250] vsize: 143228 Current children cumulated CPU time (s) 1207.96 Current children cumulated vsize (Kb) 145352 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.16 s] Raw data (loadavg): 1.04 0.99 0.96 2/57 5250 Raw data (/proc/5246/stat): 5246 (minisat+_script) S 5245 5246 31027 0 -1 0 288 239 0 0 0 0 0 1 22 0 1 0 1843273101 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5246/statm): 531 226 485 147 0 384 0 [pid=5246] vsize: 2124 Raw data (/proc/5250/stat): 5250 (minisat+_64-bit) R 5246 5246 31027 0 -1 0 34581 0 0 0 120594 201 0 0 25 0 1 0 1843273106 146665472 33675 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5250/statm): 35807 33675 145 145 0 35662 0 [pid=5250] vsize: 143228 Current children cumulated CPU time (s) 1207.96 Current children cumulated vsize (Kb) 145352 Sending SIGTERM to -5246 Sleeping 2 seconds One traced child (pid=5246) ended because it received signal 15 (SIGTERM) One traced child (pid=5250) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.22 CPU time (s): 1208.03 CPU user time (s): 1205.95 CPU system time (s): 2.07768 CPU usage (%): 99.8184 Max. virtual memory (cumulated for all children) (Kb): 145352
ERROR: no interpretation found !