Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-blp-ic98.opb |
MD5SUM | 9ca02e5a1540510bce8e96ecb8f82d9c |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 83886080000000 |
Number of bits of the biggest number in a constraint | 47 |
Biggest sum of numbers in a constraint | 783292842349555 |
Number of bits of the biggest sum of numbers | 50 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 15501 |
Total number of constraints | 14313 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 14177 |
Number of constraints which are nor clauses,nor cardinality constraints | 136 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 13581 |
LAUNCH ON wulflinc20 THE 2005-09-20 01:56:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3097 boxname=wulflinc20 idbench=753 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9ca02e5a1540510bce8e96ecb8f82d9c /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb IDLAUNCH: 3097 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 911956 kB Buffers: 132 kB Cached: 92928 kB SwapCached: 780 kB Active: 35016 kB Inactive: 60660 kB HighTotal: 131008 kB HighFree: 33992 kB LowTotal: 903652 kB LowFree: 877964 kB SwapTotal: 2097892 kB SwapFree: 2096552 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5632 kB Slab: 21284 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:16:47 (client local time) WITH STATUS 0 IN 996.233 SECONDS stats: 3097 7 996.233 0
c Parsing PB file... c PARSE ERROR! [line 27287] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 853 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########################################################################################## c -- Clauses(.)/Splits(s): sssss c ---[ 857]---> BDD-cost: 12 c ---[ 856]---> BDD-cost: 12 c ---[ 855]---> BDD-cost: 13 c ---[ 854]---> BDD-cost: 13 c ---[ 853]---> BDD-cost: 13 c ---[ 850]---> BDD-cost: 13 c ---[ 849]---> BDD-cost: 13 c ---[ 848]---> BDD-cost: 13 c ---[ 847]---> BDD-cost: 13 c ---[ 846]---> BDD-cost: 13 c ---[ 845]---> BDD-cost: 12 c ---[ 844]---> BDD-cost: 13 c ---[ 842]---> BDD-cost: 13 c ---[ 841]---> BDD-cost: 13 c ---[ 840]---> BDD-cost: 13 c ---[ 839]---> BDD-cost: 13 c ---[ 838]---> BDD-cost: 13 c ---[ 837]---> BDD-cost: 13 c ---[ 836]---> BDD-cost: 13 c ---[ 835]---> BDD-cost: 12 c ---[ 834]---> BDD-cost: 13 c ---[ 833]---> BDD-cost: 13 c ---[ 832]---> BDD-cost: 13 c ---[ 831]---> BDD-cost: 12 c ---[ 830]---> BDD-cost: 12 c ---[ 829]---> BDD-cost: 13 c ---[ 828]---> BDD-cost: 13 c ---[ 827]---> BDD-cost: 13 c ---[ 826]---> BDD-cost: 13 c ---[ 825]---> BDD-cost: 12 c ---[ 824]---> BDD-cost: 13 c ---[ 822]---> BDD-cost: 12 c ---[ 821]---> BDD-cost: 13 c ---[ 820]---> BDD-cost: 13 c ---[ 819]---> BDD-cost: 13 c ---[ 818]---> BDD-cost: 13 c ---[ 817]---> BDD-cost: 13 c ---[ 815]---> BDD-cost: 13 c ---[ 814]---> BDD-cost: 13 c ---[ 813]---> BDD-cost: 13 c ---[ 812]---> BDD-cost: 12 c ---[ 810]---> Adder-cost: 2530 maxlim: 1873920 bits: 21/21 c ---[ 808]---> Adder-cost: 954 maxlim: 966656 bits: 20/20 c ---[ 806]---> Adder-cost: 6532 maxlim: 4710400 bits: 23/23 c ---[ 804]---> Adder-cost: 1924 maxlim: 1470464 bits: 21/21 c ---[ 802]---> Adder-cost: 428 maxlim: 339968 bits: 19/19 c ---[ 800]---> Adder-cost: 10296 maxlim: 7658496 bits: 23/23 c ---[ 798]---> Adder-cost: 4976 maxlim: 5065728 bits: 23/23 c ---[ 796]---> Adder-cost: 2746 maxlim: 3383296 bits: 22/22 c ---[ 794]---> Adder-cost: 3164 maxlim: 2670592 bits: 22/22 c ---[ 792]---> Adder-cost: 2142 maxlim: 1794048 bits: 21/21 c ---[ 790]---> Adder-cost: 1618 maxlim: 1335296 bits: 21/21 c ---[ 788]---> Adder-cost: 3844 maxlim: 4069376 bits: 22/22 c ---[ 786]---> Adder-cost: 2790 maxlim: 2551808 bits: 22/22 c ---[ 784]---> Adder-cost: 962 maxlim: 854016 bits: 20/20 c ---[ 782]---> Adder-cost: 1114 maxlim: 930816 bits: 20/20 c ---[ 780]---> Adder-cost: 1356 maxlim: 1298432 bits: 21/21 c ---[ 778]---> Adder-cost: 2260 maxlim: 1982464 bits: 21/21 c ---[ 776]---> Adder-cost: 2598 maxlim: 2123776 bits: 22/22 c ---[ 774]---> Adder-cost: 1746 maxlim: 1540096 bits: 21/21 c ---[ 772]---> Adder-cost: 2930 maxlim: 2441216 bits: 22/22 c ---[ 770]---> Adder-cost: 1820 maxlim: 1594368 bits: 21/21 c ---[ 768]---> Adder-cost: 4014 maxlim: 3783680 bits: 22/22 c ---[ 766]---> Adder-cost: 6654 maxlim: 6837248 bits: 23/23 c ---[ 764]---> Adder-cost: 2044 maxlim: 1741824 bits: 21/21 c ---[ 762]---> Adder-cost: 1242 maxlim: 1152000 bits: 21/21 c ---[ 760]---> Adder-cost: 268 maxlim: 339968 bits: 19/19 c ---[ 758]---> Adder-cost: 1576 maxlim: 2551808 bits: 22/22 c ---[ 756]---> Adder-cost: 2740 maxlim: 2395136 bits: 22/22 c ---[ 754]---> Adder-cost: 2394 maxlim: 2307072 bits: 22/22 c ---[ 752]---> Adder-cost: 5924 maxlim: 5430272 bits: 23/23 c ---[ 750]---> Adder-cost: 4334 maxlim: 4377600 bits: 23/23 c ---[ 748]---> Adder-cost: 942 maxlim: 1334272 bits: 21/21 c ---[ 746]---> Adder-cost: 4304 maxlim: 4227072 bits: 23/23 c ---[ 744]---> Adder-cost: 784 maxlim: 715776 bits: 20/20 c ---[ 742]---> Adder-cost: 4446 maxlim: 4887552 bits: 23/23 c ---[ 740]---> Adder-cost: 3354 maxlim: 3956736 bits: 22/22 c ---[ 738]---> Adder-cost: 802 maxlim: 850944 bits: 20/20 c ---[ 736]---> Adder-cost: 1286 maxlim: 1291264 bits: 21/21 c ---[ 734]---> Adder-cost: 1962 maxlim: 1976320 bits: 21/21 c ---[ 732]---> Adder-c
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/27513/stat): 27513 (minisat+_script) R 27512 27513 2660 0 -1 0 19 0 0 0 0 0 0 0 20 0 1 0 1854745915 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27513/statm): 174 3 169 147 0 27 0 [pid=27513] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=27514 New process pid=27515 New process pid=27516 execve syscall for /bin/sed executable One traced child (pid=27515) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=27516) exited with status: 0 One traced child (pid=27514) exited with status: 0 New process pid=27517 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb [startup+10.0036 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 338 0 0 0 987 4 0 0 25 0 1 0 1854745920 1798144 324 4294967295 134512640 135094434 3221224432 3221223328 134588031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 439 324 145 145 0 294 0 [pid=27517] vsize: 1756 Current children cumulated CPU time (s) 9.93 Current children cumulated vsize (Kb) 3880 [startup+20.0043 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 476 0 0 0 1985 5 0 0 25 0 1 0 1854745920 2682880 459 4294967295 134512640 135094434 3221224432 3221223300 134796009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 655 459 145 145 0 510 0 [pid=27517] vsize: 2620 Current children cumulated CPU time (s) 19.92 Current children cumulated vsize (Kb) 4744 [startup+30.0041 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 549 0 0 0 2984 5 0 0 25 0 1 0 1854745920 2854912 532 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 697 532 145 145 0 552 0 [pid=27517] vsize: 2788 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 4912 [startup+40.0058 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 577 0 0 0 3983 6 0 0 25 0 1 0 1854745920 2871296 560 4294967295 134512640 135094434 3221224432 3221223328 134587994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 701 560 145 145 0 556 0 [pid=27517] vsize: 2804 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 4928 [startup+50.0065 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 621 0 0 0 4982 7 0 0 25 0 1 0 1854745920 2965504 604 4294967295 134512640 135094434 3221224432 3221223300 134796021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 724 604 145 145 0 579 0 [pid=27517] vsize: 2896 Current children cumulated CPU time (s) 49.91 Current children cumulated vsize (Kb) 5020 [startup+60.0062 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 816 0 0 0 5978 9 0 0 25 0 1 0 1854745920 3710976 725 4294967295 134512640 135094434 3221224432 3221223324 134795992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 906 725 145 145 0 761 0 [pid=27517] vsize: 3624 Current children cumulated CPU time (s) 59.89 Current children cumulated vsize (Kb) 5748 [startup+70.0069 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 823 0 0 0 6976 11 0 0 25 0 1 0 1854745920 3760128 732 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 918 732 145 145 0 773 0 [pid=27517] vsize: 3672 Current children cumulated CPU time (s) 69.89 Current children cumulated vsize (Kb) 5796 [startup+80.0077 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1073 0 0 0 7973 13 0 0 25 0 1 0 1854745920 4374528 786 4294967295 134512640 135094434 3221224432 3221223316 134796012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 1068 786 145 145 0 923 0 [pid=27517] vsize: 4272 Current children cumulated CPU time (s) 79.88 Current children cumulated vsize (Kb) 6396 [startup+90.0084 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1268 0 0 0 8970 15 0 0 25 0 1 0 1854745920 5083136 849 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 1241 849 145 145 0 1096 0 [pid=27517] vsize: 4964 Current children cumulated CPU time (s) 89.87 Current children cumulated vsize (Kb) 7088 [startup+100.009 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1394 0 0 0 9968 16 0 0 25 0 1 0 1854745920 5603328 905 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 1368 905 145 145 0 1223 0 [pid=27517] vsize: 5472 Current children cumulated CPU time (s) 99.86 Current children cumulated vsize (Kb) 7596 [startup+110.01 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1459 0 0 0 10966 17 0 0 25 0 1 0 1854745920 5861376 970 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 1431 970 145 145 0 1286 0 [pid=27517] vsize: 5724 Current children cumulated CPU time (s) 109.85 Current children cumulated vsize (Kb) 7848 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1613 0 0 0 11963 19 0 0 25 0 1 0 1854745920 6549504 1124 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 1599 1124 145 145 0 1454 0 [pid=27517] vsize: 6396 Current children cumulated CPU time (s) 119.84 Current children cumulated vsize (Kb) 8520 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) T 27513 27513 2660 0 -1 0 1686 0 0 0 12960 20 0 0 25 0 1 0 1854745920 6823936 1147 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/27517/statm): 1666 1147 145 145 0 1521 0 [pid=27517] vsize: 6664 Current children cumulated CPU time (s) 129.82 Current children cumulated vsize (Kb) 8788 [startup+140.012 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1858 0 0 0 13958 21 0 0 25 0 1 0 1854745920 7430144 1197 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 1814 1197 145 145 0 1669 0 [pid=27517] vsize: 7256 Current children cumulated CPU time (s) 139.81 Current children cumulated vsize (Kb) 9380 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 1978 0 0 0 14957 22 0 0 25 0 1 0 1854745920 7942144 1317 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 1939 1317 145 145 0 1794 0 [pid=27517] vsize: 7756 Current children cumulated CPU time (s) 149.81 Current children cumulated vsize (Kb) 9880 [startup+160.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2171 0 0 0 15954 23 0 0 25 0 1 0 1854745920 8667136 1374 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27517/statm): 2116 1374 145 145 0 1971 0 [pid=27517] vsize: 8464 Current children cumulated CPU time (s) 159.79 Current children cumulated vsize (Kb) 10588 [startup+170.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2280 0 0 0 16950 24 0 0 25 0 1 0 1854745920 9035776 1411 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 2206 1411 145 145 0 2061 0 [pid=27517] vsize: 8824 Current children cumulated CPU time (s) 169.76 Current children cumulated vsize (Kb) 10948 [startup+180.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2468 0 0 0 17947 25 0 0 25 0 1 0 1854745920 9654272 1456 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 2357 1456 145 145 0 2212 0 [pid=27517] vsize: 9428 Current children cumulated CPU time (s) 179.74 Current children cumulated vsize (Kb) 11552 [startup+190.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2513 0 0 0 18945 26 0 0 25 0 1 0 1854745920 9961472 1501 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 2432 1501 145 145 0 2287 0 [pid=27517] vsize: 9728 Current children cumulated CPU time (s) 189.73 Current children cumulated vsize (Kb) 11852 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2680 0 0 0 19943 28 0 0 25 0 1 0 1854745920 10514432 1540 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 2567 1540 145 145 0 2422 0 [pid=27517] vsize: 10268 Current children cumulated CPU time (s) 199.73 Current children cumulated vsize (Kb) 12392 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27517 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 289 239 0 0 0 1 0 1 20 0 1 0 1854745915 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27513/statm): 531 226 485 147 0 384 0 [pid=27513] vsize: 2124 Raw data (/proc/27517/stat): 27517 (minisat+_64-bit) R 27513 27513 2660 0 -1 0 2841 0 0 0 20940 29 0 0 25 0 1 0 1854745920 11022336 1580 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27517/statm): 2691 1580 145 145 0 2546 0 [pid=27517] vsize: 10764 Current children cumulated CPU time (s) 209.71 Current children cumulated vsize (Kb) 12888 One traced child (pid=27517) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=27518 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-blp-ic98.opb [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 339 0 0 0 934 3 0 0 25 0 1 0 1854766977 1859584 324 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 454 324 162 162 0 292 0 [pid=27518] vsize: 1816 Current children cumulated CPU time (s) 219.66 Current children cumulated vsize (Kb) 3944 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 480 0 0 0 1931 5 0 0 25 0 1 0 1854766977 2760704 462 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 674 462 162 162 0 512 0 [pid=27518] vsize: 2696 Current children cumulated CPU time (s) 229.65 Current children cumulated vsize (Kb) 4824 [startup+240.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 548 0 0 0 2930 7 0 0 25 0 1 0 1854766977 2932736 530 4294967295 134512640 135167914 3221224448 3221223280 134608445 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 716 530 162 162 0 554 0 [pid=27518] vsize: 2864 Current children cumulated CPU time (s) 239.66 Current children cumulated vsize (Kb) 4992 [startup+250.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 572 0 0 0 3928 8 0 0 25 0 1 0 1854766977 2932736 554 4294967295 134512640 135167914 3221224448 3221223268 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 716 554 162 162 0 554 0 [pid=27518] vsize: 2864 Current children cumulated CPU time (s) 249.65 Current children cumulated vsize (Kb) 4992 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 610 0 0 0 4927 9 0 0 25 0 1 0 1854766977 3018752 592 4294967295 134512640 135167914 3221224448 3221223268 134860174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 737 592 162 162 0 575 0 [pid=27518] vsize: 2948 Current children cumulated CPU time (s) 259.65 Current children cumulated vsize (Kb) 5076 [startup+270.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 749 0 0 0 5925 10 0 0 25 0 1 0 1854766977 3538944 731 4294967295 134512640 135167914 3221224448 3221223360 134572026 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 864 731 162 162 0 702 0 [pid=27518] vsize: 3456 Current children cumulated CPU time (s) 269.64 Current children cumulated vsize (Kb) 5584 [startup+280.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 1016 0 0 0 6920 13 0 0 25 0 1 0 1854766977 4149248 880 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1013 880 162 162 0 851 0 [pid=27518] vsize: 4052 Current children cumulated CPU time (s) 279.62 Current children cumulated vsize (Kb) 6180 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 1714 0 0 0 7912 18 0 0 25 0 1 0 1854766977 5042176 1032 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1231 1032 162 162 0 1069 0 [pid=27518] vsize: 4924 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 7052 [startup+300.022 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 1918 0 0 0 8909 20 0 0 25 0 1 0 1854766977 5861376 1236 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1431 1236 162 162 0 1269 0 [pid=27518] vsize: 5724 Current children cumulated CPU time (s) 299.58 Current children cumulated vsize (Kb) 7852 [startup+310.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2127 0 0 0 9904 23 0 0 25 0 1 0 1854766977 6062080 1285 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1480 1285 162 162 0 1318 0 [pid=27518] vsize: 5920 Current children cumulated CPU time (s) 309.56 Current children cumulated vsize (Kb) 8048 [startup+320.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2332 0 0 0 10901 24 0 0 25 0 1 0 1854766977 6914048 1490 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1688 1490 162 162 0 1526 0 [pid=27518] vsize: 6752 Current children cumulated CPU time (s) 319.54 Current children cumulated vsize (Kb) 8880 [startup+330.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2448 0 0 0 11899 25 0 0 25 0 1 0 1854766977 6955008 1503 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 1698 1503 162 162 0 1536 0 [pid=27518] vsize: 6792 Current children cumulated CPU time (s) 329.53 Current children cumulated vsize (Kb) 8920 [startup+340.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2665 0 0 0 12895 26 0 0 25 0 1 0 1854766977 7843840 1720 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 1915 1720 162 162 0 1753 0 [pid=27518] vsize: 7660 Current children cumulated CPU time (s) 339.5 Current children cumulated vsize (Kb) 9788 [startup+350.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 2828 0 0 0 13891 28 0 0 25 0 1 0 1854766977 8527872 1883 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2082 1883 162 162 0 1920 0 [pid=27518] vsize: 8328 Current children cumulated CPU time (s) 349.48 Current children cumulated vsize (Kb) 10456 [startup+360.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3221 0 0 0 14886 31 0 0 25 0 1 0 1854766977 9027584 2009 4294967295 134512640 135167914 3221224448 3221223284 134860186 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2204 2009 162 162 0 2042 0 [pid=27518] vsize: 8816 Current children cumulated CPU time (s) 359.46 Current children cumulated vsize (Kb) 10944 [startup+370.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3366 0 0 0 15884 31 0 0 25 0 1 0 1854766977 9621504 2154 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2349 2154 162 162 0 2187 0 [pid=27518] vsize: 9396 Current children cumulated CPU time (s) 369.44 Current children cumulated vsize (Kb) 11524 [startup+380.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3644 0 0 0 16880 34 0 0 25 0 1 0 1854766977 10760192 2432 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2627 2432 162 162 0 2465 0 [pid=27518] vsize: 10508 Current children cumulated CPU time (s) 379.43 Current children cumulated vsize (Kb) 12636 [startup+390.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 3837 0 0 0 17876 35 0 0 25 0 1 0 1854766977 11018240 2493 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2690 2493 162 162 0 2528 0 [pid=27518] vsize: 10760 Current children cumulated CPU time (s) 389.4 Current children cumulated vsize (Kb) 12888 [startup+400.027 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 4092 0 0 0 18871 38 0 0 25 0 1 0 1854766977 11649024 2645 4294967295 134512640 135167914 3221224448 3221222556 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2844 2645 162 162 0 2682 0 [pid=27518] vsize: 11376 Current children cumulated CPU time (s) 399.38 Current children cumulated vsize (Kb) 13504 [startup+410.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4244 0 0 0 19867 39 0 0 25 0 1 0 1854766977 12267520 2797 4294967295 134512640 135167914 3221224448 3221223284 134860186 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 2995 2797 162 162 0 2833 0 [pid=27518] vsize: 11980 Current children cumulated CPU time (s) 409.35 Current children cumulated vsize (Kb) 14108 [startup+420.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4263 0 0 0 20865 40 0 0 25 0 1 0 1854766977 12333056 2816 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 3011 2816 162 162 0 2849 0 [pid=27518] vsize: 12044 Current children cumulated CPU time (s) 419.34 Current children cumulated vsize (Kb) 14172 [startup+430.028 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 4699 0 0 0 21859 43 0 0 25 0 1 0 1854766977 13123584 3009 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 3204 3009 162 162 0 3042 0 [pid=27518] vsize: 12816 Current children cumulated CPU time (s) 429.31 Current children cumulated vsize (Kb) 14944 [startup+440.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5071 0 0 0 22854 45 0 0 25 0 1 0 1854766977 14118912 3249 4294967295 134512640 135167914 3221224448 3221223292 134860190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 3447 3249 162 162 0 3285 0 [pid=27518] vsize: 13788 Current children cumulated CPU time (s) 439.28 Current children cumulated vsize (Kb) 15916 [startup+450.029 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5193 0 0 0 23850 47 0 0 25 0 1 0 1854766977 14610432 3371 4294967295 134512640 135167914 3221224448 3221223312 134608300 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 3567 3371 162 162 0 3405 0 [pid=27518] vsize: 14268 Current children cumulated CPU time (s) 449.26 Current children cumulated vsize (Kb) 16396 [startup+460.03 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5195 0 0 0 24847 48 0 0 25 0 1 0 1854766977 14610432 3373 4294967295 134512640 135167914 3221224448 3221223312 134608335 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 3567 3373 162 162 0 3405 0 [pid=27518] vsize: 14268 Current children cumulated CPU time (s) 459.24 Current children cumulated vsize (Kb) 16396 [startup+470.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 5195 0 0 0 25845 49 0 0 25 0 1 0 1854766977 14610432 3373 4294967295 134512640 135167914 3221224448 3221223284 134860181 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 3567 3373 162 162 0 3405 0 [pid=27518] vsize: 14268 Current children cumulated CPU time (s) 469.23 Current children cumulated vsize (Kb) 16396 [startup+480.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 6444 0 0 0 26833 55 0 0 25 0 1 0 1854766977 16707584 3887 4294967295 134512640 135167914 3221224448 3221223312 134608332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4079 3887 162 162 0 3917 0 [pid=27518] vsize: 16316 Current children cumulated CPU time (s) 479.17 Current children cumulated vsize (Kb) 18444 [startup+490.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 6545 0 0 0 27831 56 0 0 25 0 1 0 1854766977 17117184 3988 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4179 3988 162 162 0 4017 0 [pid=27518] vsize: 16716 Current children cumulated CPU time (s) 489.16 Current children cumulated vsize (Kb) 18844 [startup+500.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7152 0 0 0 28823 60 0 0 25 0 1 0 1854766977 17616896 4050 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4301 4050 162 162 0 4139 0 [pid=27518] vsize: 17204 Current children cumulated CPU time (s) 499.12 Current children cumulated vsize (Kb) 19332 [startup+510.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7353 0 0 0 29820 62 0 0 25 0 1 0 1854766977 18440192 4251 4294967295 134512640 135167914 3221224448 3221220460 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4502 4251 162 162 0 4340 0 [pid=27518] vsize: 18008 Current children cumulated CPU time (s) 509.11 Current children cumulated vsize (Kb) 20136 [startup+520.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7577 0 0 0 30816 64 0 0 25 0 1 0 1854766977 18690048 4313 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4563 4313 162 162 0 4401 0 [pid=27518] vsize: 18252 Current children cumulated CPU time (s) 519.09 Current children cumulated vsize (Kb) 20380 [startup+530.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7775 0 0 0 31814 65 0 0 25 0 1 0 1854766977 19501056 4511 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4761 4511 162 162 0 4599 0 [pid=27518] vsize: 19044 Current children cumulated CPU time (s) 529.08 Current children cumulated vsize (Kb) 21172 [startup+540.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 7862 0 0 0 32812 66 0 0 25 0 1 0 1854766977 19853312 4598 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 4847 4598 162 162 0 4685 0 [pid=27518] vsize: 19388 Current children cumulated CPU time (s) 539.07 Current children cumulated vsize (Kb) 21516 [startup+550.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8018 0 0 0 33809 67 0 0 25 0 1 0 1854766977 20484096 4754 4294967295 134512640 135167914 3221224448 3221223312 134608307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 5001 4754 162 162 0 4839 0 [pid=27518] vsize: 20004 Current children cumulated CPU time (s) 549.05 Current children cumulated vsize (Kb) 22132 [startup+560.034 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8175 0 0 0 34805 69 0 0 25 0 1 0 1854766977 21143552 4911 4294967295 134512640 135167914 3221224448 3221223284 134860172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 5162 4911 162 162 0 5000 0 [pid=27518] vsize: 20648 Current children cumulated CPU time (s) 559.03 Current children cumulated vsize (Kb) 22776 [startup+570.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8606 0 0 0 35800 71 0 0 25 0 1 0 1854766977 21790720 5074 4294967295 134512640 135167914 3221224448 3221223284 134860164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 5320 5074 162 162 0 5158 0 [pid=27518] vsize: 21280 Current children cumulated CPU time (s) 569 Current children cumulated vsize (Kb) 23408 [startup+580.035 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8705 0 0 0 36797 73 0 0 25 0 1 0 1854766977 22196224 5173 4294967295 134512640 135167914 3221224448 3221223312 134608298 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 5419 5173 162 162 0 5257 0 [pid=27518] vsize: 21676 Current children cumulated CPU time (s) 578.99 Current children cumulated vsize (Kb) 23804 [startup+590.036 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 8997 0 0 0 37791 75 0 0 25 0 1 0 1854766977 23396352 5465 4294967295 134512640 135167914 3221224448 3221223284 134860188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 5712 5465 162 162 0 5550 0 [pid=27518] vsize: 22848 Current children cumulated CPU time (s) 588.95 Current children cumulated vsize (Kb) 24976 [startup+600.036 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9111 0 0 0 38788 76 0 0 25 0 1 0 1854766977 23416832 5476 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 5717 5476 162 162 0 5555 0 [pid=27518] vsize: 22868 Current children cumulated CPU time (s) 598.93 Current children cumulated vsize (Kb) 24996 [startup+610.037 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9413 0 0 0 39782 79 0 0 25 0 1 0 1854766977 24662016 5778 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 6021 5778 162 162 0 5859 0 [pid=27518] vsize: 24084 Current children cumulated CPU time (s) 608.9 Current children cumulated vsize (Kb) 26212 [startup+620.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9436 0 0 0 40781 80 0 0 25 0 1 0 1854766977 24735744 5801 4294967295 134512640 135167914 3221224448 3221223284 134860174 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 6039 5801 162 162 0 5877 0 [pid=27518] vsize: 24156 Current children cumulated CPU time (s) 618.9 Current children cumulated vsize (Kb) 26284 [startup+630.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 9866 0 0 0 41776 83 0 0 25 0 1 0 1854766977 25526272 5988 4294967295 134512640 135167914 3221224448 3221223312 134608296 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 6232 5988 162 162 0 6070 0 [pid=27518] vsize: 24928 Current children cumulated CPU time (s) 628.88 Current children cumulated vsize (Kb) 27056 [startup+640.038 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10073 0 0 0 42772 84 0 0 25 0 1 0 1854766977 25804800 6063 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 6300 6063 162 162 0 6138 0 [pid=27518] vsize: 25200 Current children cumulated CPU time (s) 638.85 Current children cumulated vsize (Kb) 27328 [startup+650.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10371 0 0 0 43766 87 0 0 25 0 1 0 1854766977 27033600 6361 4294967295 134512640 135167914 3221224448 3221223284 134860166 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 6600 6361 162 162 0 6438 0 [pid=27518] vsize: 26400 Current children cumulated CPU time (s) 648.82 Current children cumulated vsize (Kb) 28528 [startup+660.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10371 0 0 0 44765 88 0 0 25 0 1 0 1854766977 27033600 6361 4294967295 134512640 135167914 3221224448 3221223284 134860169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 6600 6361 162 162 0 6438 0 [pid=27518] vsize: 26400 Current children cumulated CPU time (s) 658.82 Current children cumulated vsize (Kb) 28528 [startup+670.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 10381 0 0 0 45763 88 0 0 25 0 1 0 1854766977 27090944 6371 4294967295 134512640 135167914 3221224448 3221223296 134608317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 6614 6371 162 162 0 6452 0 [pid=27518] vsize: 26456 Current children cumulated CPU time (s) 668.8 Current children cumulated vsize (Kb) 28584 [startup+680.039 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 12623 0 0 0 46748 97 0 0 25 0 1 0 1854766977 34770944 8228 4294967295 134512640 135167914 3221224448 3221080156 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 8489 8228 162 162 0 8327 0 [pid=27518] vsize: 33956 Current children cumulated CPU time (s) 678.74 Current children cumulated vsize (Kb) 36084 [startup+690.04 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14649 0 0 0 47737 104 0 0 25 0 1 0 1854766977 41537536 9812 4294967295 134512640 135167914 3221224448 3221223112 134847007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 10141 9812 162 162 0 9979 0 [pid=27518] vsize: 40564 Current children cumulated CPU time (s) 688.7 Current children cumulated vsize (Kb) 42692 [startup+700.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14649 0 0 0 48737 104 0 0 25 0 1 0 1854766977 41537536 9812 4294967295 134512640 135167914 3221224448 3221221408 134718203 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 10141 9812 162 162 0 9979 0 [pid=27518] vsize: 40564 Current children cumulated CPU time (s) 698.7 Current children cumulated vsize (Kb) 42692 [startup+710.041 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 49737 104 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221223112 134846907 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0 [pid=27518] vsize: 40696 Current children cumulated CPU time (s) 708.7 Current children cumulated vsize (Kb) 42824 [startup+720.042 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 50737 105 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221221404 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0 [pid=27518] vsize: 40696 Current children cumulated CPU time (s) 718.71 Current children cumulated vsize (Kb) 42824 [startup+730.043 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 14743 0 0 0 51737 105 0 0 25 0 1 0 1854766977 41672704 9906 4294967295 134512640 135167914 3221224448 3221221072 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 10174 9906 162 162 0 10012 0 [pid=27518] vsize: 40696 Current children cumulated CPU time (s) 728.71 Current children cumulated vsize (Kb) 42824 [startup+740.044 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 15002 0 0 0 52734 106 0 0 25 0 1 0 1854766977 45424640 10165 4294967295 134512640 135167914 3221224448 3221223168 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 11090 10165 162 162 0 10928 0 [pid=27518] vsize: 44360 Current children cumulated CPU time (s) 738.69 Current children cumulated vsize (Kb) 46488 [startup+750.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 19870 0 0 0 53695 124 0 0 25 0 1 0 1854766977 62824448 14413 4294967295 134512640 135167914 3221224448 3219998112 134845149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 15338 14413 162 162 0 15176 0 [pid=27518] vsize: 61352 Current children cumulated CPU time (s) 748.48 Current children cumulated vsize (Kb) 63480 [startup+760.045 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 24650 0 0 0 54655 143 0 0 25 0 1 0 1854766977 79704064 18534 4294967295 134512640 135167914 3221224448 3219027520 134624395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 19459 18534 162 162 0 19297 0 [pid=27518] vsize: 77836 Current children cumulated CPU time (s) 758.27 Current children cumulated vsize (Kb) 79964 [startup+770.046 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 30516 0 0 0 55611 166 0 0 25 0 1 0 1854766977 98332672 23082 4294967295 134512640 135167914 3221224448 3218836288 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 24007 23082 162 162 0 23845 0 [pid=27518] vsize: 96028 Current children cumulated CPU time (s) 768.06 Current children cumulated vsize (Kb) 98156 [startup+780.046 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 34283 0 0 0 56569 184 0 0 25 0 1 0 1854766977 113762304 26849 4294967295 134512640 135167914 3221224448 3220005028 134849147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 27774 26849 162 162 0 27612 0 [pid=27518] vsize: 111096 Current children cumulated CPU time (s) 777.82 Current children cumulated vsize (Kb) 113224 [startup+790.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 42446 0 0 0 57523 211 0 0 25 0 1 0 1854766977 136396800 32375 4294967295 134512640 135167914 3221224448 3219625164 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 33300 32375 162 162 0 33138 0 [pid=27518] vsize: 133200 Current children cumulated CPU time (s) 787.63 Current children cumulated vsize (Kb) 135328 [startup+800.048 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 46173 0 0 0 58479 231 0 0 25 0 1 0 1854766977 151662592 36102 4294967295 134512640 135167914 3221224448 3219825136 134625053 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 37027 36102 162 162 0 36865 0 [pid=27518] vsize: 148108 Current children cumulated CPU time (s) 797.39 Current children cumulated vsize (Kb) 150236 [startup+810.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 49784 0 0 0 59440 246 0 0 25 0 1 0 1854766977 166453248 39713 4294967295 134512640 135167914 3221224448 3219698944 134621141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 40638 39713 162 162 0 40476 0 [pid=27518] vsize: 162552 Current children cumulated CPU time (s) 807.15 Current children cumulated vsize (Kb) 164680 [startup+820.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 53337 0 0 0 60401 262 0 0 25 0 1 0 1854766977 181006336 43266 4294967295 134512640 135167914 3221224448 3219298536 134846958 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 44191 43266 162 162 0 44029 0 [pid=27518] vsize: 176764 Current children cumulated CPU time (s) 816.92 Current children cumulated vsize (Kb) 178892 [startup+830.049 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 56943 0 0 0 61361 281 0 0 25 0 1 0 1854766977 195776512 46872 4294967295 134512640 135167914 3221224448 3219982232 134843032 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 47797 46872 162 162 0 47635 0 [pid=27518] vsize: 191188 Current children cumulated CPU time (s) 826.71 Current children cumulated vsize (Kb) 193316 [startup+840.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 69649 0 0 0 62313 316 0 0 25 0 1 0 1854766977 226222080 54305 4294967295 134512640 135167914 3221224448 3219294576 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 55230 54305 162 162 0 55068 0 [pid=27518] vsize: 220920 Current children cumulated CPU time (s) 836.58 Current children cumulated vsize (Kb) 223048 [startup+850.051 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 73302 0 0 0 63271 333 0 0 25 0 1 0 1854766977 241184768 57958 4294967295 134512640 135167914 3221224448 3219260028 134722576 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 58883 57958 162 162 0 58721 0 [pid=27518] vsize: 235532 Current children cumulated CPU time (s) 846.33 Current children cumulated vsize (Kb) 237660 [startup+860.05 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 77016 0 0 0 64228 352 0 0 25 0 1 0 1854766977 256397312 61672 4294967295 134512640 135167914 3221224448 3219539848 134844633 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 62597 61672 162 162 0 62435 0 [pid=27518] vsize: 250388 Current children cumulated CPU time (s) 856.09 Current children cumulated vsize (Kb) 252516 [startup+870.051 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 80688 0 0 0 65184 371 0 0 25 0 1 0 1854766977 271437824 65344 4294967295 134512640 135167914 3221224448 3220781944 134845939 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 66269 65344 162 162 0 66107 0 [pid=27518] vsize: 265076 Current children cumulated CPU time (s) 865.84 Current children cumulated vsize (Kb) 267204 [startup+880.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 84366 0 0 0 66142 389 0 0 25 0 1 0 1854766977 286502912 69022 4294967295 134512640 135167914 3221224448 3220424832 134845197 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 69947 69022 162 162 0 69785 0 [pid=27518] vsize: 279788 Current children cumulated CPU time (s) 875.6 Current children cumulated vsize (Kb) 281916 [startup+890.052 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 88118 0 0 0 67099 408 0 0 25 0 1 0 1854766977 301871104 72774 4294967295 134512640 135167914 3221224448 3220499036 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 73699 72774 162 162 0 73537 0 [pid=27518] vsize: 294796 Current children cumulated CPU time (s) 885.36 Current children cumulated vsize (Kb) 296924 [startup+900.053 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 91874 0 0 0 68056 427 0 0 25 0 1 0 1854766977 317255680 76530 4294967295 134512640 135167914 3221224448 3220024928 134844697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 77455 76530 162 162 0 77293 0 [pid=27518] vsize: 309820 Current children cumulated CPU time (s) 895.12 Current children cumulated vsize (Kb) 311948 [startup+910.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 95678 0 0 0 69015 445 0 0 25 0 1 0 1854766977 332836864 80334 4294967295 134512640 135167914 3221224448 3219853568 134845702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 81259 80334 162 162 0 81097 0 [pid=27518] vsize: 325036 Current children cumulated CPU time (s) 904.89 Current children cumulated vsize (Kb) 327164 [startup+920.055 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 99500 0 0 0 69974 462 0 0 25 0 1 0 1854766977 348491776 84156 4294967295 134512640 135167914 3221224448 3220294016 134844767 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 85081 84156 162 162 0 84919 0 [pid=27518] vsize: 340324 Current children cumulated CPU time (s) 914.65 Current children cumulated vsize (Kb) 342452 [startup+930.054 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 121355 0 0 0 70918 513 0 0 25 0 1 0 1854766977 438009856 106011 4294967295 134512640 135167914 3221224448 3218198992 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 106936 106011 162 162 0 106774 0 [pid=27518] vsize: 427744 Current children cumulated CPU time (s) 924.6 Current children cumulated vsize (Kb) 429872 [startup+940.055 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 125163 0 0 0 71871 536 0 0 25 0 1 0 1854766977 410411008 99273 4294967295 134512640 135167914 3221224448 3218407564 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 100198 99273 162 162 0 100036 0 [pid=27518] vsize: 400792 Current children cumulated CPU time (s) 934.36 Current children cumulated vsize (Kb) 402920 [startup+950.056 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 129211 0 0 0 72823 557 0 0 25 0 1 0 1854766977 426995712 103321 4294967295 134512640 135167914 3221224448 3219865660 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 104247 103321 162 162 0 104085 0 [pid=27518] vsize: 416988 Current children cumulated CPU time (s) 944.09 Current children cumulated vsize (Kb) 419116 [startup+960.056 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 133201 0 0 0 73775 577 0 0 25 0 1 0 1854766977 443334656 107311 4294967295 134512640 135167914 3221224448 3219403996 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 108236 107311 162 162 0 108074 0 [pid=27518] vsize: 432944 Current children cumulated CPU time (s) 953.81 Current children cumulated vsize (Kb) 435072 [startup+970.056 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 137274 0 0 0 74730 596 0 0 25 0 1 0 1854766977 460017664 111384 4294967295 134512640 135167914 3221224448 3218287484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 112309 111384 162 162 0 112147 0 [pid=27518] vsize: 449236 Current children cumulated CPU time (s) 963.55 Current children cumulated vsize (Kb) 451364 [startup+980.056 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 141391 0 0 0 75682 618 0 0 25 0 1 0 1854766977 476880896 115501 4294967295 134512640 135167914 3221224448 3218208508 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 116426 115501 162 162 0 116264 0 [pid=27518] vsize: 465704 Current children cumulated CPU time (s) 973.29 Current children cumulated vsize (Kb) 467832 [startup+990.057 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 145475 0 0 0 76634 637 0 0 25 0 1 0 1854766977 493608960 119585 4294967295 134512640 135167914 3221224448 3219558576 134844653 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 120510 119585 162 162 0 120348 0 [pid=27518] vsize: 482040 Current children cumulated CPU time (s) 983 Current children cumulated vsize (Kb) 484168 [startup+1000.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 149612 0 0 0 77586 657 0 0 25 0 1 0 1854766977 510554112 123722 4294967295 134512640 135167914 3221224448 3218209488 134624410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 124647 123722 162 162 0 124485 0 [pid=27518] vsize: 498588 Current children cumulated CPU time (s) 992.72 Current children cumulated vsize (Kb) 500716 [startup+1010.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 153702 0 0 0 78538 676 0 0 25 0 1 0 1854766977 527306752 127812 4294967295 134512640 135167914 3221224448 3218206016 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 128737 127812 162 162 0 128575 0 [pid=27518] vsize: 514948 Current children cumulated CPU time (s) 1002.43 Current children cumulated vsize (Kb) 517076 [startup+1020.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 157703 0 0 0 79492 696 0 0 25 0 1 0 1854766977 543694848 131813 4294967295 134512640 135167914 3221224448 3220033360 134849163 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 132738 131813 162 162 0 132576 0 [pid=27518] vsize: 530952 Current children cumulated CPU time (s) 1012.17 Current children cumulated vsize (Kb) 533080 [startup+1030.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 161824 0 0 0 80446 715 0 0 25 0 1 0 1854766977 560574464 135934 4294967295 134512640 135167914 3221224448 3220218012 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 136859 135934 162 162 0 136697 0 [pid=27518] vsize: 547436 Current children cumulated CPU time (s) 1021.9 Current children cumulated vsize (Kb) 549564 [startup+1040.06 s] Raw data (loadavg): 0.99 0.97 0.92 1/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 165895 0 0 0 81401 733 0 0 25 0 1 0 1854766977 577249280 140005 4294967295 134512640 135167914 3221224448 3218321596 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 140930 140005 162 162 0 140768 0 [pid=27518] vsize: 563720 Current children cumulated CPU time (s) 1031.63 Current children cumulated vsize (Kb) 565848 [startup+1050.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 170072 0 0 0 82358 753 0 0 25 0 1 0 1854766977 594358272 144182 4294967295 134512640 135167914 3221224448 3218219484 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 145107 144182 162 162 0 144945 0 [pid=27518] vsize: 580428 Current children cumulated CPU time (s) 1041.4 Current children cumulated vsize (Kb) 582556 [startup+1060.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 174148 0 0 0 83310 773 0 0 25 0 1 0 1854766977 611053568 148258 4294967295 134512640 135167914 3221224448 3219464924 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 149183 148258 162 162 0 149021 0 [pid=27518] vsize: 596732 Current children cumulated CPU time (s) 1051.12 Current children cumulated vsize (Kb) 598860 [startup+1070.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 178245 0 0 0 84264 793 0 0 25 0 1 0 1854766977 627834880 152355 4294967295 134512640 135167914 3221224448 3218192072 134722513 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 153280 152355 162 162 0 153118 0 [pid=27518] vsize: 613120 Current children cumulated CPU time (s) 1060.86 Current children cumulated vsize (Kb) 615248 [startup+1080.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 182282 0 0 0 85217 812 0 0 25 0 1 0 1854766977 644370432 156392 4294967295 134512640 135167914 3221224448 3218217604 134849086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 157317 156392 162 162 0 157155 0 [pid=27518] vsize: 629268 Current children cumulated CPU time (s) 1070.58 Current children cumulated vsize (Kb) 631396 [startup+1090.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 227074 0 0 0 86085 926 0 0 25 0 1 0 1854766977 827838464 201184 4294967295 134512640 135167914 3221224448 3219792976 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 202109 201184 162 162 0 201947 0 [pid=27518] vsize: 808436 Current children cumulated CPU time (s) 1080.4 Current children cumulated vsize (Kb) 810564 [startup+1100.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 227074 0 0 0 87085 926 0 0 25 0 1 0 1854766977 827838464 201184 4294967295 134512640 135167914 3221224448 3219792976 134694392 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 202109 201184 162 162 0 201947 0 [pid=27518] vsize: 808436 Current children cumulated CPU time (s) 1090.4 Current children cumulated vsize (Kb) 810564 [startup+1110.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 230187 0 0 0 88043 944 0 0 25 0 1 0 1854766977 754200576 183206 4294967295 134512640 135167914 3221224448 3219858720 134849440 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 184131 183206 162 162 0 183969 0 [pid=27518] vsize: 736524 Current children cumulated CPU time (s) 1100.16 Current children cumulated vsize (Kb) 738652 [startup+1120.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 234467 0 0 0 88993 967 0 0 25 0 1 0 1854766977 771731456 187486 4294967295 134512640 135167914 3221224448 3218278340 134619308 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 188411 187486 162 162 0 188249 0 [pid=27518] vsize: 753644 Current children cumulated CPU time (s) 1109.89 Current children cumulated vsize (Kb) 755772 [startup+1130.06 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 238633 0 0 0 89945 988 0 0 25 0 1 0 1854766977 788795392 191652 4294967295 134512640 135167914 3221224448 3218281976 134849558 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 192577 191652 162 162 0 192415 0 [pid=27518] vsize: 770308 Current children cumulated CPU time (s) 1119.62 Current children cumulated vsize (Kb) 772436 [startup+1140.07 s] Raw data (loadavg): 1.07 0.99 0.93 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 242860 0 0 0 90896 1008 0 0 25 0 1 0 1854766977 806109184 195879 4294967295 134512640 135167914 3221224448 3220208928 134522497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 196804 195879 162 162 0 196642 0 [pid=27518] vsize: 787216 Current children cumulated CPU time (s) 1129.33 Current children cumulated vsize (Kb) 789344 [startup+1150.07 s] Raw data (loadavg): 1.06 0.99 0.93 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) T 27513 27513 2660 0 -1 0 247070 0 0 0 91847 1030 0 0 25 0 1 0 1854766977 823353344 200089 4294967295 134512640 135167914 3221224448 3218184284 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27518/statm): 201014 200089 162 162 0 200852 0 [pid=27518] vsize: 804056 Current children cumulated CPU time (s) 1139.06 Current children cumulated vsize (Kb) 806184 [startup+1160.07 s] Raw data (loadavg): 1.05 0.99 0.93 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 251259 0 0 0 92803 1050 0 0 25 0 1 0 1854766977 840511488 204278 4294967295 134512640 135167914 3221224448 3218240284 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 205203 204278 162 162 0 205041 0 [pid=27518] vsize: 820812 Current children cumulated CPU time (s) 1148.82 Current children cumulated vsize (Kb) 822940 [startup+1170.07 s] Raw data (loadavg): 1.11 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 255495 0 0 0 93754 1071 0 0 25 0 1 0 1854766977 857862144 208514 4294967295 134512640 135167914 3221224448 3218207760 134849061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 209439 208514 162 162 0 209277 0 [pid=27518] vsize: 837756 Current children cumulated CPU time (s) 1158.54 Current children cumulated vsize (Kb) 839884 [startup+1180.07 s] Raw data (loadavg): 1.10 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 259648 0 0 0 94709 1091 0 0 25 0 1 0 1854766977 874872832 212667 4294967295 134512640 135167914 3221224448 3219732960 134849196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 213592 212667 162 162 0 213430 0 [pid=27518] vsize: 854368 Current children cumulated CPU time (s) 1168.29 Current children cumulated vsize (Kb) 856496 [startup+1190.07 s] Raw data (loadavg): 1.08 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 263868 0 0 0 95661 1111 0 0 25 0 1 0 1854766977 892157952 216887 4294967295 134512640 135167914 3221224448 3218251744 134845937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 217812 216887 162 162 0 217650 0 [pid=27518] vsize: 871248 Current children cumulated CPU time (s) 1178.01 Current children cumulated vsize (Kb) 873376 [startup+1200.07 s] Raw data (loadavg): 1.07 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 268022 0 0 0 96612 1132 0 0 25 0 1 0 1854766977 909172736 221041 4294967295 134512640 135167914 3221224448 3218273588 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 221966 221041 162 162 0 221804 0 [pid=27518] vsize: 887864 Current children cumulated CPU time (s) 1187.73 Current children cumulated vsize (Kb) 889992 [startup+1210.07 s] Raw data (loadavg): 1.06 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 272224 0 0 0 97561 1155 0 0 25 0 1 0 1854766977 926384128 225243 4294967295 134512640 135167914 3221224448 3218270712 134694321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27518/statm): 226168 225243 162 162 0 226006 0 [pid=27518] vsize: 904672 Current children cumulated CPU time (s) 1197.45 Current children cumulated vsize (Kb) 906800 [startup+1220.07 s] Raw data (loadavg): 1.05 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 277105 0 58 0 98404 1176 0 0 21 0 1 0 1854766977 940875776 224614 4294967295 134512640 135167914 3221224448 3218211488 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 229706 224614 162 162 0 229544 0 [pid=27518] vsize: 918824 Current children cumulated CPU time (s) 1206.09 Current children cumulated vsize (Kb) 920952 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1220.07 s] Raw data (loadavg): 1.05 1.00 0.94 2/57 27518 Raw data (/proc/27513/stat): 27513 (minisat+_script) S 27512 27513 2660 0 -1 0 314 3195 0 0 0 1 20996 32 19 0 1 0 1854745915 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27513/statm): 532 234 485 147 0 385 0 [pid=27513] vsize: 2128 Raw data (/proc/27518/stat): 27518 (minisat+_bignum) R 27513 27513 2660 0 -1 0 277105 0 58 0 98404 1176 0 0 21 0 1 0 1854766977 940875776 224614 4294967295 134512640 135167914 3221224448 3218211488 134844728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27518/statm): 229706 224614 162 162 0 229544 0 [pid=27518] vsize: 918824 Current children cumulated CPU time (s) 1206.09 Current children cumulated vsize (Kb) 920952 Sending SIGTERM to -27513 Sleeping 2 seconds One traced child (pid=27513) ended because it received signal 15 (SIGTERM) One traced child (pid=27518) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1220.5 CPU time (s): 996.233 CPU user time (s): 984.047 CPU system time (s): 12.1851 CPU usage (%): 81.6251 Max. virtual memory (cumulated for all children) (Kb): 920952
ERROR: no interpretation found !