Name | mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-markshare2_1.opb |
MD5SUM | 375b355299c9fbf8170e172bcbc73eb2 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 9786 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 7340025 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 7340025 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.36 |
Number of variables | 242 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 54 |
Number of constraints which are nor clauses,nor cardinality constraints | 13 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 122 |
LAUNCH ON wulflinc1 THE 2005-09-20 05:11:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3444 boxname=wulflinc1 idbench=1100 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 375b355299c9fbf8170e172bcbc73eb2 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb IDLAUNCH: 3444 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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: 867244 kB Buffers: 14296 kB Cached: 123808 kB SwapCached: 1160 kB Active: 40288 kB Inactive: 100448 kB HighTotal: 131008 kB HighFree: 23884 kB LowTotal: 903652 kB LowFree: 843360 kB SwapTotal: 2097136 kB SwapFree: 2095268 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5764 kB Slab: 20760 kB Committed_AS: 92624 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:31:54 (client local time) WITH STATUS 10 IN 1209.4 SECONDS stats: 3444 7 1209.4 10
c Parsing PB file... c Converting 20 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 19]---> BDD-cost: 7 c ---[ 18]---> BDD-cost: 7 c ---[ 17]---> BDD-cost: 7 c ---[ 16]---> BDD-cost: 7 c ---[ 15]---> BDD-cost: 7 c ---[ 14]---> BDD-cost: 7 c ---[ 12]---> Adder-cost: 590 maxlim: 469334 bits: 20/19 c ---[ 10]---> Adder-cost: 648 maxlim: 507792 bits: 20/19 c ---[ 8]---> Adder-cost: 604 maxlim: 482140 bits: 20/19 c ---[ 6]---> Adder-cost: 572 maxlim: 518845 bits: 20/19 c ---[ 4]---> Adder-cost: 688 maxlim: 476350 bits: 20/19 c ---[ 2]---> Adder-cost: 646 maxlim: 516106 bits: 20/19 c ---[ 0]---> Adder-cost: 598 maxlim: 472356 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 29589 105189 | 9863 0 0 nan | 0.000 % | c | 100 | 29589 105189 | 10849 100 294 2.9 | 6.191 % | c | 250 | 29589 105189 | 11934 250 1546 6.2 | 6.191 % | c ============================================================================== c [1mFound solution: 895884[0m c ---[ 0]---> Sorter-cost: 1831 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 420 | 34259 116094 | 11419 420 3527 8.4 | 6.191 % | c ============================================================================== c [1mFound solution: 277009[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 442 | 34312 116266 | 11437 442 3696 8.4 | 6.191 % | c | 542 | 34312 116266 | 12580 542 19307 35.6 | 4.622 % | c | 692 | 34312 116266 | 13838 692 20278 29.3 | 4.622 % | c | 919 | 34304 116240 | 15222 918 23363 25.4 | 4.638 % | c | 1256 | 34296 116214 | 16744 1254 26303 21.0 | 4.654 % | c | 1762 | 34282 116183 | 18419 1758 31387 17.9 | 4.716 % | c | 2523 | 34274 116157 | 20261 2518 52135 20.7 | 4.732 % | c | 3663 | 34266 116131 | 22287 3657 86430 23.6 | 4.748 % | c | 5371 | 34258 116105 | 24516 5364 157198 29.3 | 4.763 % | c | 7933 | 34250 116079 | 26967 7925 283775 35.8 | 4.779 % | c | 11777 | 34232 116039 | 29664 11766 467502 39.7 | 4.857 % | c | 17545 | 34232 116039 | 32631 17534 744678 42.5 | 4.857 % | c | 26194 | 34232 116039 | 35894 26183 1229982 47.0 | 4.857 % | c | 39168 | 34232 116039 | 39483 16577 675473 40.7 | 4.857 % | c | 58629 | 34224 116013 | 43431 36037 1748106 48.5 | 4.873 % | c | 87821 | 34216 115987 | 47775 35097 1973601 56.2 | 4.889 % | c | 131610 | 34216 115987 | 52552 44264 2632869 59.5 | 4.889 % | c | 197294 | 34208 115965 | 57807 34890 2157751 61.8 | 4.920 % | c | 295820 | 34194 115921 | 63588 47108 2866807 60.9 | 4.951 % | c | 443610 | 34185 115894 | 69947 48453 3071079 63.4 | 4.983 % |
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/21747/stat): 21747 (minisat+_script) R 21746 21747 10120 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 1740834517 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/21747/statm): 174 3 169 147 0 27 0 [pid=21747] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script open syscall for file /usr/lib/gconv/gconv-modules.cache New process pid=21748 New process pid=21749 New process pid=21750 execve syscall for /bin/sed executable One traced child (pid=21749) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6 open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6 open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6 open syscall for file /usr/local/globus-2.4.3/lib/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 open syscall for file /usr/lib/locale/locale-archive open syscall for file /usr/lib/gconv/gconv-modules.cache One traced child (pid=21750) exited with status: 0 One traced child (pid=21748) exited with status: 0 New process pid=21751 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-markshare2_1.opb [startup+10.0036 s] Raw data (loadavg): 0.93 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 1512 0 0 0 977 8 0 0 25 0 1 0 1740834524 6512640 1463 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 1590 1463 145 145 0 1445 0 [pid=21751] vsize: 6360 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 10556 [startup+20.0054 s] Raw data (loadavg): 0.94 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 2149 0 0 0 1964 13 0 0 25 0 1 0 1740834524 9142272 2100 4294967295 134512640 135094434 3221221600 3221220256 134557896 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 2232 2100 145 145 0 2087 0 [pid=21751] vsize: 8928 Current children cumulated CPU time (s) 19.79 Current children cumulated vsize (Kb) 13124 [startup+30.0062 s] Raw data (loadavg): 0.95 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 2668 0 0 0 2953 18 0 0 25 0 1 0 1740834524 11235328 2619 4294967295 134512640 135094434 3221221600 3221220256 134558208 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 2743 2619 145 145 0 2598 0 [pid=21751] vsize: 10972 Current children cumulated CPU time (s) 29.73 Current children cumulated vsize (Kb) 15168 [startup+40.007 s] Raw data (loadavg): 0.95 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 3947 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220272 134556410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0 [pid=21751] vsize: 12476 Current children cumulated CPU time (s) 39.7 Current children cumulated vsize (Kb) 16672 [startup+50.0078 s] Raw data (loadavg): 0.96 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 4947 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220236 134557560 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0 [pid=21751] vsize: 12476 Current children cumulated CPU time (s) 49.7 Current children cumulated vsize (Kb) 16672 [startup+60.0086 s] Raw data (loadavg): 0.97 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3017 0 0 0 5946 21 0 0 25 0 1 0 1740834524 12775424 2968 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 3119 2968 145 145 0 2974 0 [pid=21751] vsize: 12476 Current children cumulated CPU time (s) 59.69 Current children cumulated vsize (Kb) 16672 [startup+70.0094 s] Raw data (loadavg): 0.97 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3295 0 0 0 6941 24 0 0 25 0 1 0 1740834524 13901824 3246 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 3394 3246 145 145 0 3249 0 [pid=21751] vsize: 13576 Current children cumulated CPU time (s) 69.67 Current children cumulated vsize (Kb) 17772 [startup+80.0101 s] Raw data (loadavg): 0.98 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 7933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220240 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0 [pid=21751] vsize: 15260 Current children cumulated CPU time (s) 79.62 Current children cumulated vsize (Kb) 19456 [startup+90.0109 s] Raw data (loadavg): 0.98 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 8933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220192 134557488 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0 [pid=21751] vsize: 15260 Current children cumulated CPU time (s) 89.62 Current children cumulated vsize (Kb) 19456 [startup+100.011 s] Raw data (loadavg): 0.98 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3721 0 0 0 9933 27 0 0 25 0 1 0 1740834524 15626240 3672 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 3815 3672 145 145 0 3670 0 [pid=21751] vsize: 15260 Current children cumulated CPU time (s) 99.62 Current children cumulated vsize (Kb) 19456 [startup+110.011 s] Raw data (loadavg): 0.98 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 3762 0 0 0 10932 27 0 0 25 0 1 0 1740834524 15798272 3713 4294967295 134512640 135094434 3221221600 3221220256 134558123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 3857 3713 145 145 0 3712 0 [pid=21751] vsize: 15428 Current children cumulated CPU time (s) 109.61 Current children cumulated vsize (Kb) 19624 [startup+120.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4157 0 0 0 11923 31 0 0 25 0 1 0 1740834524 17408000 4108 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4250 4108 145 145 0 4105 0 [pid=21751] vsize: 17000 Current children cumulated CPU time (s) 119.56 Current children cumulated vsize (Kb) 21196 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 12921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0 [pid=21751] vsize: 17616 Current children cumulated CPU time (s) 129.56 Current children cumulated vsize (Kb) 21812 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 13921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0 [pid=21751] vsize: 17616 Current children cumulated CPU time (s) 139.56 Current children cumulated vsize (Kb) 21812 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 14921 33 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220256 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0 [pid=21751] vsize: 17616 Current children cumulated CPU time (s) 149.56 Current children cumulated vsize (Kb) 21812 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 15921 34 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220264 134556595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0 [pid=21751] vsize: 17616 Current children cumulated CPU time (s) 159.57 Current children cumulated vsize (Kb) 21812 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4313 0 0 0 16921 34 0 0 25 0 1 0 1740834524 18038784 4264 4294967295 134512640 135094434 3221221600 3221220272 134555957 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4404 4264 145 145 0 4259 0 [pid=21751] vsize: 17616 Current children cumulated CPU time (s) 169.57 Current children cumulated vsize (Kb) 21812 [startup+180.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4573 0 0 0 17916 36 0 0 25 0 1 0 1740834524 19103744 4524 4294967295 134512640 135094434 3221221600 3221220192 134557352 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 4664 4524 145 145 0 4519 0 [pid=21751] vsize: 18656 Current children cumulated CPU time (s) 179.54 Current children cumulated vsize (Kb) 22852 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 18908 39 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0 [pid=21751] vsize: 20020 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 24216 [startup+200.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 19908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0 [pid=21751] vsize: 20020 Current children cumulated CPU time (s) 199.5 Current children cumulated vsize (Kb) 24216 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 20908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0 [pid=21751] vsize: 20020 Current children cumulated CPU time (s) 209.5 Current children cumulated vsize (Kb) 24216 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 21909 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0 [pid=21751] vsize: 20020 Current children cumulated CPU time (s) 219.51 Current children cumulated vsize (Kb) 24216 [startup+230.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4918 0 0 0 22908 40 0 0 25 0 1 0 1740834524 20500480 4869 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5005 4869 145 145 0 4860 0 [pid=21751] vsize: 20020 Current children cumulated CPU time (s) 229.5 Current children cumulated vsize (Kb) 24216 [startup+240.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4933 0 0 0 23909 40 0 0 25 0 1 0 1740834524 20582400 4884 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5025 4884 145 145 0 4880 0 [pid=21751] vsize: 20100 Current children cumulated CPU time (s) 239.51 Current children cumulated vsize (Kb) 24296 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 24908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220288 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0 [pid=21751] vsize: 20352 Current children cumulated CPU time (s) 249.5 Current children cumulated vsize (Kb) 24548 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 25908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0 [pid=21751] vsize: 20352 Current children cumulated CPU time (s) 259.5 Current children cumulated vsize (Kb) 24548 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 26908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0 [pid=21751] vsize: 20352 Current children cumulated CPU time (s) 269.5 Current children cumulated vsize (Kb) 24548 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 4996 0 0 0 27908 40 0 0 25 0 1 0 1740834524 20840448 4947 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5088 4947 145 145 0 4943 0 [pid=21751] vsize: 20352 Current children cumulated CPU time (s) 279.5 Current children cumulated vsize (Kb) 24548 [startup+290.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5021 0 0 0 28908 40 0 0 25 0 1 0 1740834524 20946944 4972 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5114 4972 145 145 0 4969 0 [pid=21751] vsize: 20456 Current children cumulated CPU time (s) 289.5 Current children cumulated vsize (Kb) 24652 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5384 0 0 0 29901 44 0 0 25 0 1 0 1740834524 22425600 5335 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5475 5335 145 145 0 5330 0 [pid=21751] vsize: 21900 Current children cumulated CPU time (s) 299.47 Current children cumulated vsize (Kb) 26096 [startup+310.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 30899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 309.46 Current children cumulated vsize (Kb) 26804 [startup+320.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 31899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 319.46 Current children cumulated vsize (Kb) 26804 [startup+330.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 32899 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220272 134555599 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 329.46 Current children cumulated vsize (Kb) 26804 [startup+340.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 33900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 339.47 Current children cumulated vsize (Kb) 26804 [startup+350.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 34900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557843 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 349.47 Current children cumulated vsize (Kb) 26804 [startup+360.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5564 0 0 0 35900 45 0 0 25 0 1 0 1740834524 23150592 5515 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5652 5515 145 145 0 5507 0 [pid=21751] vsize: 22608 Current children cumulated CPU time (s) 359.47 Current children cumulated vsize (Kb) 26804 [startup+370.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 5739 0 0 0 36897 46 0 0 25 0 1 0 1740834524 23871488 5690 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 5828 5690 145 145 0 5683 0 [pid=21751] vsize: 23312 Current children cumulated CPU time (s) 369.45 Current children cumulated vsize (Kb) 27508 [startup+380.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6064 0 0 0 37891 49 0 0 25 0 1 0 1740834524 25214976 6015 4294967295 134512640 135094434 3221221600 3221220192 134556809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6156 6015 145 145 0 6011 0 [pid=21751] vsize: 24624 Current children cumulated CPU time (s) 379.42 Current children cumulated vsize (Kb) 28820 [startup+390.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 38890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 389.41 Current children cumulated vsize (Kb) 28932 [startup+400.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 39890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 399.41 Current children cumulated vsize (Kb) 28932 [startup+410.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 40890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 409.41 Current children cumulated vsize (Kb) 28932 [startup+420.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 41890 49 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 419.41 Current children cumulated vsize (Kb) 28932 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 42890 50 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 429.42 Current children cumulated vsize (Kb) 28932 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6093 0 0 0 43889 50 0 0 25 0 1 0 1740834524 25329664 6044 4294967295 134512640 135094434 3221221600 3221220256 134558035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 6184 6044 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 439.41 Current children cumulated vsize (Kb) 28932 [startup+450.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6097 0 0 0 44889 50 0 0 25 0 1 0 1740834524 25329664 6048 4294967295 134512640 135094434 3221221600 3221220264 134556595 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6184 6048 145 145 0 6039 0 [pid=21751] vsize: 24736 Current children cumulated CPU time (s) 449.41 Current children cumulated vsize (Kb) 28932 [startup+460.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 45887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220192 134557191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 459.4 Current children cumulated vsize (Kb) 29356 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 46887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 469.4 Current children cumulated vsize (Kb) 29356 [startup+480.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 47887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 479.4 Current children cumulated vsize (Kb) 29356 [startup+490.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 48887 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 489.4 Current children cumulated vsize (Kb) 29356 [startup+500.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 49888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 499.41 Current children cumulated vsize (Kb) 29356 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 50888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 509.41 Current children cumulated vsize (Kb) 29356 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 51888 51 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 519.41 Current children cumulated vsize (Kb) 29356 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 52888 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 529.42 Current children cumulated vsize (Kb) 29356 [startup+540.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 53888 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 539.42 Current children cumulated vsize (Kb) 29356 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 54889 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 549.43 Current children cumulated vsize (Kb) 29356 [startup+560.043 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6205 0 0 0 55889 52 0 0 25 0 1 0 1740834524 25763840 6156 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6290 6156 145 145 0 6145 0 [pid=21751] vsize: 25160 Current children cumulated CPU time (s) 559.43 Current children cumulated vsize (Kb) 29356 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6275 0 0 0 56888 52 0 0 25 0 1 0 1740834524 26050560 6226 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6360 6226 145 145 0 6215 0 [pid=21751] vsize: 25440 Current children cumulated CPU time (s) 569.42 Current children cumulated vsize (Kb) 29636 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6435 0 0 0 57886 53 0 0 25 0 1 0 1740834524 26734592 6386 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6527 6386 145 145 0 6382 0 [pid=21751] vsize: 26108 Current children cumulated CPU time (s) 579.41 Current children cumulated vsize (Kb) 30304 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6435 0 0 0 58886 53 0 0 25 0 1 0 1740834524 26734592 6386 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6527 6386 145 145 0 6382 0 [pid=21751] vsize: 26108 Current children cumulated CPU time (s) 589.41 Current children cumulated vsize (Kb) 30304 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6445 0 0 0 59886 53 0 0 25 0 1 0 1740834524 26832896 6396 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6551 6396 145 145 0 6406 0 [pid=21751] vsize: 26204 Current children cumulated CPU time (s) 599.41 Current children cumulated vsize (Kb) 30400 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6456 0 0 0 60886 53 0 0 25 0 1 0 1740834524 26865664 6407 4294967295 134512640 135094434 3221221600 3221220256 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6559 6407 145 145 0 6414 0 [pid=21751] vsize: 26236 Current children cumulated CPU time (s) 609.41 Current children cumulated vsize (Kb) 30432 [startup+620.047 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6457 0 0 0 61886 53 0 0 25 0 1 0 1740834524 26865664 6408 4294967295 134512640 135094434 3221221600 3221220256 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6559 6408 145 145 0 6414 0 [pid=21751] vsize: 26236 Current children cumulated CPU time (s) 619.41 Current children cumulated vsize (Kb) 30432 [startup+630.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6473 0 0 0 62887 53 0 0 25 0 1 0 1740834524 26963968 6424 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6583 6424 145 145 0 6438 0 [pid=21751] vsize: 26332 Current children cumulated CPU time (s) 629.42 Current children cumulated vsize (Kb) 30528 [startup+640.048 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6473 0 0 0 63887 53 0 0 25 0 1 0 1740834524 26963968 6424 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6583 6424 145 145 0 6438 0 [pid=21751] vsize: 26332 Current children cumulated CPU time (s) 639.42 Current children cumulated vsize (Kb) 30528 [startup+650.049 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6480 0 0 0 64887 53 0 0 25 0 1 0 1740834524 26996736 6431 4294967295 134512640 135094434 3221221600 3221220272 134556610 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6591 6431 145 145 0 6446 0 [pid=21751] vsize: 26364 Current children cumulated CPU time (s) 649.42 Current children cumulated vsize (Kb) 30560 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6486 0 0 0 65887 53 0 0 25 0 1 0 1740834524 27029504 6437 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6599 6437 145 145 0 6454 0 [pid=21751] vsize: 26396 Current children cumulated CPU time (s) 659.42 Current children cumulated vsize (Kb) 30592 [startup+670.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6486 0 0 0 66887 53 0 0 25 0 1 0 1740834524 27029504 6437 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6599 6437 145 145 0 6454 0 [pid=21751] vsize: 26396 Current children cumulated CPU time (s) 669.42 Current children cumulated vsize (Kb) 30592 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6487 0 0 0 67888 53 0 0 25 0 1 0 1740834524 27029504 6438 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6599 6438 145 145 0 6454 0 [pid=21751] vsize: 26396 Current children cumulated CPU time (s) 679.43 Current children cumulated vsize (Kb) 30592 [startup+690.052 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6527 0 0 0 68888 54 0 0 25 0 1 0 1740834524 27291648 6478 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6663 6478 145 145 0 6518 0 [pid=21751] vsize: 26652 Current children cumulated CPU time (s) 689.44 Current children cumulated vsize (Kb) 30848 [startup+700.053 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6589 0 0 0 69887 54 0 0 25 0 1 0 1740834524 27594752 6540 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6737 6540 145 145 0 6592 0 [pid=21751] vsize: 26948 Current children cumulated CPU time (s) 699.43 Current children cumulated vsize (Kb) 31144 [startup+710.054 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6787 0 0 0 70883 56 0 0 25 0 1 0 1740834524 28397568 6738 4294967295 134512640 135094434 3221221600 3221220256 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6933 6738 145 145 0 6788 0 [pid=21751] vsize: 27732 Current children cumulated CPU time (s) 709.41 Current children cumulated vsize (Kb) 31928 [startup+720.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 71881 57 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0 [pid=21751] vsize: 27884 Current children cumulated CPU time (s) 719.4 Current children cumulated vsize (Kb) 32080 [startup+730.055 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 72881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0 [pid=21751] vsize: 27884 Current children cumulated CPU time (s) 729.41 Current children cumulated vsize (Kb) 32080 [startup+740.056 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 73881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0 [pid=21751] vsize: 27884 Current children cumulated CPU time (s) 739.41 Current children cumulated vsize (Kb) 32080 [startup+750.057 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6826 0 0 0 74881 58 0 0 25 0 1 0 1740834524 28553216 6777 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6971 6777 145 145 0 6826 0 [pid=21751] vsize: 27884 Current children cumulated CPU time (s) 749.41 Current children cumulated vsize (Kb) 32080 [startup+760.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6832 0 0 0 75881 59 0 0 25 0 1 0 1740834524 28581888 6783 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6978 6783 145 145 0 6833 0 [pid=21751] vsize: 27912 Current children cumulated CPU time (s) 759.42 Current children cumulated vsize (Kb) 32108 [startup+770.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6833 0 0 0 76881 59 0 0 25 0 1 0 1740834524 28581888 6784 4294967295 134512640 135094434 3221221600 3221220256 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6978 6784 145 145 0 6833 0 [pid=21751] vsize: 27912 Current children cumulated CPU time (s) 769.42 Current children cumulated vsize (Kb) 32108 [startup+780.058 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6839 0 0 0 77881 59 0 0 25 0 1 0 1740834524 28614656 6790 4294967295 134512640 135094434 3221221600 3221220288 134554687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6986 6790 145 145 0 6841 0 [pid=21751] vsize: 27944 Current children cumulated CPU time (s) 779.42 Current children cumulated vsize (Kb) 32140 [startup+790.059 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6846 0 0 0 78882 59 0 0 25 0 1 0 1740834524 28647424 6797 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 6994 6797 145 145 0 6849 0 [pid=21751] vsize: 27976 Current children cumulated CPU time (s) 789.43 Current children cumulated vsize (Kb) 32172 [startup+800.06 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6858 0 0 0 79881 59 0 0 25 0 1 0 1740834524 28712960 6809 4294967295 134512640 135094434 3221221600 3221220256 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7010 6809 145 145 0 6865 0 [pid=21751] vsize: 28040 Current children cumulated CPU time (s) 799.42 Current children cumulated vsize (Kb) 32236 [startup+810.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6868 0 0 0 80881 59 0 0 25 0 1 0 1740834524 28778496 6819 4294967295 134512640 135094434 3221221600 3221220256 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7026 6819 145 145 0 6881 0 [pid=21751] vsize: 28104 Current children cumulated CPU time (s) 809.42 Current children cumulated vsize (Kb) 32300 [startup+820.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6868 0 0 0 81881 59 0 0 25 0 1 0 1740834524 28778496 6819 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7026 6819 145 145 0 6881 0 [pid=21751] vsize: 28104 Current children cumulated CPU time (s) 819.42 Current children cumulated vsize (Kb) 32300 [startup+830.062 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 6936 0 0 0 82880 60 0 0 25 0 1 0 1740834524 29057024 6887 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7094 6887 145 145 0 6949 0 [pid=21751] vsize: 28376 Current children cumulated CPU time (s) 829.42 Current children cumulated vsize (Kb) 32572 [startup+840.063 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7186 0 0 0 83875 62 0 0 25 0 1 0 1740834524 30351360 7137 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7410 7137 145 145 0 7265 0 [pid=21751] vsize: 29640 Current children cumulated CPU time (s) 839.39 Current children cumulated vsize (Kb) 33836 [startup+850.064 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7360 0 0 0 84871 63 0 0 25 0 1 0 1740834524 31072256 7311 4294967295 134512640 135094434 3221221600 3221220256 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7311 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 849.36 Current children cumulated vsize (Kb) 34540 [startup+860.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7360 0 0 0 85871 64 0 0 25 0 1 0 1740834524 31072256 7311 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7311 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 859.37 Current children cumulated vsize (Kb) 34540 [startup+870.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7362 0 0 0 86871 64 0 0 25 0 1 0 1740834524 31072256 7313 4294967295 134512640 135094434 3221221600 3221220256 134557934 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7313 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 869.37 Current children cumulated vsize (Kb) 34540 [startup+880.065 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7364 0 0 0 87872 64 0 0 25 0 1 0 1740834524 31072256 7315 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7315 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 879.38 Current children cumulated vsize (Kb) 34540 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 88872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220192 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 889.38 Current children cumulated vsize (Kb) 34540 [startup+900.067 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 89872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220256 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 899.38 Current children cumulated vsize (Kb) 34540 [startup+910.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7367 0 0 0 90872 64 0 0 25 0 1 0 1740834524 31072256 7318 4294967295 134512640 135094434 3221221600 3221220256 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7586 7318 145 145 0 7441 0 [pid=21751] vsize: 30344 Current children cumulated CPU time (s) 909.38 Current children cumulated vsize (Kb) 34540 [startup+920.068 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7372 0 0 0 91872 64 0 0 25 0 1 0 1740834524 31105024 7323 4294967295 134512640 135094434 3221221600 3221220256 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7594 7323 145 145 0 7449 0 [pid=21751] vsize: 30376 Current children cumulated CPU time (s) 919.38 Current children cumulated vsize (Kb) 34572 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7387 0 0 0 92873 64 0 0 25 0 1 0 1740834524 31203328 7338 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7618 7338 145 145 0 7473 0 [pid=21751] vsize: 30472 Current children cumulated CPU time (s) 929.39 Current children cumulated vsize (Kb) 34668 [startup+940.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7389 0 0 0 93872 64 0 0 25 0 1 0 1740834524 31203328 7340 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7618 7340 145 145 0 7473 0 [pid=21751] vsize: 30472 Current children cumulated CPU time (s) 939.38 Current children cumulated vsize (Kb) 34668 [startup+950.071 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7422 0 0 0 94873 64 0 0 25 0 1 0 1740834524 31363072 7373 4294967295 134512640 135094434 3221221600 3221220288 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7657 7373 145 145 0 7512 0 [pid=21751] vsize: 30628 Current children cumulated CPU time (s) 949.39 Current children cumulated vsize (Kb) 34824 [startup+960.072 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7467 0 0 0 95872 65 0 0 25 0 1 0 1740834524 31539200 7418 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7700 7418 145 145 0 7555 0 [pid=21751] vsize: 30800 Current children cumulated CPU time (s) 959.39 Current children cumulated vsize (Kb) 34996 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7736 0 0 0 96867 67 0 0 25 0 1 0 1740834524 32636928 7687 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 7968 7687 145 145 0 7823 0 [pid=21751] vsize: 31872 Current children cumulated CPU time (s) 969.36 Current children cumulated vsize (Kb) 36068 [startup+980.072 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 97864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220192 134551428 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 979.35 Current children cumulated vsize (Kb) 36952 [startup+990.073 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 98864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 989.35 Current children cumulated vsize (Kb) 36952 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 99864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 999.35 Current children cumulated vsize (Kb) 36952 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 100864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220272 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1009.35 Current children cumulated vsize (Kb) 36952 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 101864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220212 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1019.35 Current children cumulated vsize (Kb) 36952 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 102864 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1029.35 Current children cumulated vsize (Kb) 36952 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 103865 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1039.36 Current children cumulated vsize (Kb) 36952 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 104865 69 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1049.36 Current children cumulated vsize (Kb) 36952 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 105865 70 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134557987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1059.37 Current children cumulated vsize (Kb) 36952 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7942 0 0 0 106865 70 0 0 25 0 1 0 1740834524 33542144 7893 4294967295 134512640 135094434 3221221600 3221220256 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8189 7893 145 145 0 8044 0 [pid=21751] vsize: 32756 Current children cumulated CPU time (s) 1069.37 Current children cumulated vsize (Kb) 36952 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 107865 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0 [pid=21751] vsize: 32820 Current children cumulated CPU time (s) 1079.37 Current children cumulated vsize (Kb) 37016 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 108865 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0 [pid=21751] vsize: 32820 Current children cumulated CPU time (s) 1089.37 Current children cumulated vsize (Kb) 37016 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7951 0 0 0 109864 70 0 0 25 0 1 0 1740834524 33607680 7902 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8205 7902 145 145 0 8060 0 [pid=21751] vsize: 32820 Current children cumulated CPU time (s) 1099.36 Current children cumulated vsize (Kb) 37016 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7956 0 0 0 110865 70 0 0 25 0 1 0 1740834524 33640448 7907 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8213 7907 145 145 0 8068 0 [pid=21751] vsize: 32852 Current children cumulated CPU time (s) 1109.37 Current children cumulated vsize (Kb) 37048 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7966 0 0 0 111865 70 0 0 25 0 1 0 1740834524 33640448 7917 4294967295 134512640 135094434 3221221600 3221220240 134558043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8213 7917 145 145 0 8068 0 [pid=21751] vsize: 32852 Current children cumulated CPU time (s) 1119.37 Current children cumulated vsize (Kb) 37048 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 112865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1129.37 Current children cumulated vsize (Kb) 37080 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 113865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1139.37 Current children cumulated vsize (Kb) 37080 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 114865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1149.37 Current children cumulated vsize (Kb) 37080 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 115865 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1159.37 Current children cumulated vsize (Kb) 37080 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 116866 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1169.38 Current children cumulated vsize (Kb) 37080 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7971 0 0 0 117866 70 0 0 25 0 1 0 1740834524 33673216 7922 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7922 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1179.38 Current children cumulated vsize (Kb) 37080 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7972 0 0 0 118866 70 0 0 25 0 1 0 1740834524 33673216 7923 4294967295 134512640 135094434 3221221600 3221220256 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7923 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1189.38 Current children cumulated vsize (Kb) 37080 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7973 0 0 0 119866 71 0 0 25 0 1 0 1740834524 33673216 7924 4294967295 134512640 135094434 3221221600 3221220256 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8221 7924 145 145 0 8076 0 [pid=21751] vsize: 32884 Current children cumulated CPU time (s) 1199.39 Current children cumulated vsize (Kb) 37080 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7982 0 0 0 120866 71 0 0 25 0 1 0 1740834524 33738752 7933 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8237 7933 145 145 0 8092 0 [pid=21751] vsize: 32948 Current children cumulated CPU time (s) 1209.39 Current children cumulated vsize (Kb) 37144 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.98 2/56 21751 Raw data (/proc/21747/stat): 21747 (minisat+_script) S 21746 21747 10120 0 -1 0 322 276 0 0 0 1 0 1 16 0 1 0 1740834517 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/21747/statm): 1049 256 1003 147 0 902 0 [pid=21747] vsize: 4196 Raw data (/proc/21751/stat): 21751 (minisat+_64-bit) R 21747 21747 10120 0 -1 0 7982 0 0 0 120866 71 0 0 25 0 1 0 1740834524 33738752 7933 4294967295 134512640 135094434 3221221600 3221220064 134780585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/21751/statm): 8237 7933 145 145 0 8092 0 [pid=21751] vsize: 32948 Current children cumulated CPU time (s) 1209.39 Current children cumulated vsize (Kb) 37144 Sending SIGTERM to -21747 Sleeping 2 seconds One traced child (pid=21747) ended because it received signal 15 (SIGTERM) One traced child (pid=21751) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.4 CPU user time (s): 1208.67 CPU system time (s): 0.727889 CPU usage (%): 99.9413 Max. virtual memory (cumulated for all children) (Kb): 37144
ERROR: no interpretation found !