Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ic98.opb |
MD5SUM | 4c475edac91e4650fa2d3e487e86c291 |
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 | 21 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 2097151 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 81920000000 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 66700085225335 |
Number of bits of the biggest sum of numbers | 46 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 14923 |
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 | 13571 |
LAUNCH ON wulflinc29 THE 2005-09-20 05:31:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3482 boxname=wulflinc29 idbench=1138 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4c475edac91e4650fa2d3e487e86c291 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb IDLAUNCH: 3482 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.020 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.020 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 823896 kB Buffers: 38640 kB Cached: 140112 kB SwapCached: 768 kB Active: 50364 kB Inactive: 130920 kB HighTotal: 131008 kB HighFree: 22484 kB LowTotal: 903652 kB LowFree: 801412 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5680 kB Slab: 23788 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:39:43 (client local time) WITH STATUS 0 IN 473.535 SECONDS stats: 3482 7 473.535 0
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: 9 c ---[ 856]---> BDD-cost: 9 c ---[ 855]---> BDD-cost: 10 c ---[ 854]---> BDD-cost: 10 c ---[ 853]---> BDD-cost: 10 c ---[ 850]---> BDD-cost: 10 c ---[ 849]---> BDD-cost: 10 c ---[ 848]---> BDD-cost: 10 c ---[ 847]---> BDD-cost: 10 c ---[ 846]---> BDD-cost: 10 c ---[ 845]---> BDD-cost: 9 c ---[ 844]---> BDD-cost: 10 c ---[ 842]---> BDD-cost: 10 c ---[ 841]---> BDD-cost: 10 c ---[ 840]---> BDD-cost: 10 c ---[ 839]---> BDD-cost: 10 c ---[ 838]---> BDD-cost: 10 c ---[ 837]---> BDD-cost: 10 c ---[ 836]---> BDD-cost: 10 c ---[ 835]---> BDD-cost: 9 c ---[ 834]---> BDD-cost: 10 c ---[ 833]---> BDD-cost: 10 c ---[ 832]---> BDD-cost: 10 c ---[ 831]---> BDD-cost: 9 c ---[ 830]---> BDD-cost: 9 c ---[ 829]---> BDD-cost: 10 c ---[ 828]---> BDD-cost: 10 c ---[ 827]---> BDD-cost: 10 c ---[ 826]---> BDD-cost: 10 c ---[ 825]---> BDD-cost: 9 c ---[ 824]---> BDD-cost: 10 c ---[ 822]---> BDD-cost: 9 c ---[ 821]---> BDD-cost: 10 c ---[ 820]---> BDD-cost: 10 c ---[ 819]---> BDD-cost: 10 c ---[ 818]---> BDD-cost: 10 c ---[ 817]---> BDD-cost: 10 c ---[ 815]---> BDD-cost: 10 c ---[ 814]---> BDD-cost: 10 c ---[ 813]---> BDD-cost: 10 c ---[ 812]---> BDD-cost: 9 c ---[ 810]---> Adder-cost: 2530 maxlim: 234240 bits: 18/18 c ---[ 808]---> Adder-cost: 954 maxlim: 120832 bits: 17/17 c ---[ 806]---> Adder-cost: 6532 maxlim: 588800 bits: 20/20 c ---[ 804]---> Adder-cost: 1924 maxlim: 183808 bits: 18/18 c ---[ 802]---> Adder-cost: 428 maxlim: 42496 bits: 16/16 c ---[ 800]---> Adder-cost: 10296 maxlim: 957312 bits: 20/20 c ---[ 798]---> Adder-cost: 4976 maxlim: 633216 bits: 20/20 c ---[ 796]---> Adder-cost: 2746 maxlim: 422912 bits: 19/19 c ---[ 794]---> Adder-cost: 3164 maxlim: 333824 bits: 19/19 c ---[ 792]---> Adder-cost: 2142 maxlim: 224256 bits: 18/18 c ---[ 790]---> Adder-cost: 1618 maxlim: 166912 bits: 18/18 c ---[ 788]---> Adder-cost: 3844 maxlim: 508672 bits: 19/19 c ---[ 786]---> Adder-cost: 2790 maxlim: 318976 bits: 19/19 c ---[ 784]---> Adder-cost: 962 maxlim: 106752 bits: 17/17 c ---[ 782]---> Adder-cost: 1114 maxlim: 116352 bits: 17/17 c ---[ 780]---> Adder-cost: 1356 maxlim: 162304 bits: 18/18 c ---[ 778]---> Adder-cost: 2260 maxlim: 247808 bits: 18/18 c ---[ 776]---> Adder-cost: 2598 maxlim: 265472 bits: 19/19 c ---[ 774]---> Adder-cost: 1746 maxlim: 192512 bits: 18/18 c ---[ 772]---> Adder-cost: 2930 maxlim: 305152 bits: 19/19 c ---[ 770]---> Adder-cost: 1820 maxlim: 199296 bits: 18/18 c ---[ 768]---> Adder-cost: 4014 maxlim: 472960 bits: 19/19 c ---[ 766]---> Adder-cost: 6654 maxlim: 854656 bits: 20/20 c ---[ 764]---> Adder-cost: 2044 maxlim: 217728 bits: 18/18 c ---[ 762]---> Adder-cost: 1242 maxlim: 144000 bits: 18/18 c ---[ 760]---> Adder-cost: 268 maxlim: 42496 bits: 16/16 c ---[ 758]---> Adder-cost: 1576 maxlim: 318976 bits: 19/19 c ---[ 756]---> Adder-cost: 2740 maxlim: 299392 bits: 19/19 c ---[ 754]---> Adder-cost: 2394 maxlim: 288384 bits: 19/19 c ---[ 752]---> Adder-cost: 5924 maxlim: 678784 bits: 20/20 c ---[ 750]---> Adder-cost: 4334 maxlim: 547200 bits: 20/20 c ---[ 748]---> Adder-cost: 942 maxlim: 166784 bits: 18/18 c ---[ 746]---> Adder-cost: 4304 maxlim: 528384 bits: 20/20 c ---[ 744]---> Adder-cost: 784 maxlim: 89472 bits: 17/17 c ---[ 742]---> Adder-cost: 4446 maxlim: 610944 bits: 20/20 c ---[ 740]---> Adder-cost: 3354 maxlim: 494592 bits: 19/19 c ---[ 738]---> Adder-cost: 802 maxlim: 106368 bits: 17/17 c ---[ 736]---> Adder-cost: 1286 maxlim: 161408 bits: 18/18 c ---[ 734]---> Adder-cost: 1962 maxlim: 247040 bits: 18/18 c ---[ 732]---> Adder-cost: 1334 maxlim: 163200 bits:
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/5778/stat): 5778 (minisat+_script) R 5777 5778 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1856027218 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/5778/statm): 174 3 169 147 0 27 0 [pid=5778] 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=5779 New process pid=5780 New process pid=5781 execve syscall for /bin/sed executable One traced child (pid=5780) 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=5781) exited with status: 0 One traced child (pid=5779) exited with status: 0 New process pid=5782 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-blp-ic98.opb [startup+10.0038 s] Raw data (loadavg): 0.93 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 347 0 0 0 986 3 0 0 25 0 1 0 1856027223 1814528 333 4294967295 134512640 135094434 3221224432 3221223300 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 443 333 145 145 0 298 0 [pid=5782] vsize: 1772 Current children cumulated CPU time (s) 9.9 Current children cumulated vsize (Kb) 3896 [startup+20.0046 s] Raw data (loadavg): 0.94 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 482 0 0 0 1984 5 0 0 25 0 1 0 1856027223 2682880 465 4294967295 134512640 135094434 3221224432 3221223300 134796010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 655 465 145 145 0 510 0 [pid=5782] vsize: 2620 Current children cumulated CPU time (s) 19.9 Current children cumulated vsize (Kb) 4744 [startup+30.0054 s] Raw data (loadavg): 0.95 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 548 0 0 0 2983 6 0 0 25 0 1 0 1856027223 2854912 531 4294967295 134512640 135094434 3221224432 3221223300 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 697 531 145 145 0 552 0 [pid=5782] vsize: 2788 Current children cumulated CPU time (s) 29.9 Current children cumulated vsize (Kb) 4912 [startup+40.0062 s] Raw data (loadavg): 0.96 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 575 0 0 0 3982 6 0 0 25 0 1 0 1856027223 2871296 558 4294967295 134512640 135094434 3221224432 3221223300 134796009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 701 558 145 145 0 556 0 [pid=5782] vsize: 2804 Current children cumulated CPU time (s) 39.89 Current children cumulated vsize (Kb) 4928 [startup+50.0079 s] Raw data (loadavg): 0.96 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 617 0 0 0 4981 8 0 0 25 0 1 0 1856027223 2961408 600 4294967295 134512640 135094434 3221224432 3221223300 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 723 600 145 145 0 578 0 [pid=5782] vsize: 2892 Current children cumulated CPU time (s) 49.9 Current children cumulated vsize (Kb) 5016 [startup+60.0087 s] Raw data (loadavg): 0.97 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 812 0 0 0 5978 9 0 0 25 0 1 0 1856027223 3702784 721 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 904 721 145 145 0 759 0 [pid=5782] vsize: 3616 Current children cumulated CPU time (s) 59.88 Current children cumulated vsize (Kb) 5740 [startup+70.0095 s] Raw data (loadavg): 0.97 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 821 0 0 0 6976 10 0 0 25 0 1 0 1856027223 3756032 730 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 917 730 145 145 0 772 0 [pid=5782] vsize: 3668 Current children cumulated CPU time (s) 69.87 Current children cumulated vsize (Kb) 5792 [startup+80.0103 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1172 0 0 0 7973 12 0 0 25 0 1 0 1856027223 4685824 801 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1144 801 145 145 0 999 0 [pid=5782] vsize: 4576 Current children cumulated CPU time (s) 79.86 Current children cumulated vsize (Kb) 6700 [startup+90.0111 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1272 0 0 0 8969 14 0 0 25 0 1 0 1856027223 5169152 854 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1262 854 145 145 0 1117 0 [pid=5782] vsize: 5048 Current children cumulated CPU time (s) 89.84 Current children cumulated vsize (Kb) 7172 [startup+100.012 s] Raw data (loadavg): 0.98 0.96 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1399 0 0 0 9967 15 0 0 25 0 1 0 1856027223 5693440 911 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1390 911 145 145 0 1245 0 [pid=5782] vsize: 5560 Current children cumulated CPU time (s) 99.83 Current children cumulated vsize (Kb) 7684 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1474 0 0 0 10965 16 0 0 25 0 1 0 1856027223 6021120 986 4294967295 134512640 135094434 3221224432 3221223316 134796010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1470 986 145 145 0 1325 0 [pid=5782] vsize: 5880 Current children cumulated CPU time (s) 109.82 Current children cumulated vsize (Kb) 8004 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1587 0 0 0 11962 17 0 0 25 0 1 0 1856027223 6520832 1099 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1592 1099 145 145 0 1447 0 [pid=5782] vsize: 6368 Current children cumulated CPU time (s) 119.8 Current children cumulated vsize (Kb) 8492 [startup+130.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1813 0 0 0 12959 19 0 0 25 0 1 0 1856027223 7249920 1153 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1770 1153 145 145 0 1625 0 [pid=5782] vsize: 7080 Current children cumulated CPU time (s) 129.79 Current children cumulated vsize (Kb) 9204 [startup+140.014 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1918 0 0 0 13956 21 0 0 25 0 1 0 1856027223 7761920 1258 4294967295 134512640 135094434 3221224432 3221223324 134796030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1895 1258 145 145 0 1750 0 [pid=5782] vsize: 7580 Current children cumulated CPU time (s) 139.78 Current children cumulated vsize (Kb) 9704 [startup+150.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 1956 0 0 0 14955 22 0 0 25 0 1 0 1856027223 7917568 1296 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 1933 1296 145 145 0 1788 0 [pid=5782] vsize: 7732 Current children cumulated CPU time (s) 149.78 Current children cumulated vsize (Kb) 9856 [startup+160.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2178 0 0 0 15951 24 0 0 25 0 1 0 1856027223 8638464 1352 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2109 1352 145 145 0 1964 0 [pid=5782] vsize: 8436 Current children cumulated CPU time (s) 159.76 Current children cumulated vsize (Kb) 10560 [startup+170.016 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2391 0 0 0 16948 26 0 0 25 0 1 0 1856027223 9367552 1421 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2287 1421 145 145 0 2142 0 [pid=5782] vsize: 9148 Current children cumulated CPU time (s) 169.75 Current children cumulated vsize (Kb) 11272 [startup+180.017 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2480 0 0 0 17945 27 0 0 25 0 1 0 1856027223 9707520 1442 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2370 1442 145 145 0 2225 0 [pid=5782] vsize: 9480 Current children cumulated CPU time (s) 179.73 Current children cumulated vsize (Kb) 11604 [startup+190.018 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2515 0 0 0 18944 28 0 0 25 0 1 0 1856027223 9924608 1477 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2423 1477 145 145 0 2278 0 [pid=5782] vsize: 9692 Current children cumulated CPU time (s) 189.73 Current children cumulated vsize (Kb) 11816 [startup+200.019 s] Raw data (loadavg): 0.99 0.97 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2758 0 0 0 19941 30 0 0 25 0 1 0 1856027223 10731520 1537 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2620 1537 145 145 0 2475 0 [pid=5782] vsize: 10480 Current children cumulated CPU time (s) 199.72 Current children cumulated vsize (Kb) 12604 [startup+210.02 s] Raw data (loadavg): 1.07 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2947 0 0 0 20938 32 0 0 25 0 1 0 1856027223 11333632 1585 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2767 1585 145 145 0 2622 0 [pid=5782] vsize: 11068 Current children cumulated CPU time (s) 209.71 Current children cumulated vsize (Kb) 13192 [startup+220.02 s] Raw data (loadavg): 1.06 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2952 0 0 0 21934 34 0 0 25 0 1 0 1856027223 11333632 1590 4294967295 134512640 135094434 3221224432 3221223344 134587864 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2767 1590 145 145 0 2622 0 [pid=5782] vsize: 11068 Current children cumulated CPU time (s) 219.69 Current children cumulated vsize (Kb) 13192 [startup+230.021 s] Raw data (loadavg): 1.05 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 2980 0 0 0 22933 35 0 0 25 0 1 0 1856027223 11497472 1618 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 2807 1618 145 145 0 2662 0 [pid=5782] vsize: 11228 Current children cumulated CPU time (s) 229.69 Current children cumulated vsize (Kb) 13352 [startup+240.022 s] Raw data (loadavg): 1.04 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3632 0 0 0 23927 38 0 0 25 0 1 0 1856027223 13299712 1759 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3247 1759 145 145 0 3102 0 [pid=5782] vsize: 12988 Current children cumulated CPU time (s) 239.66 Current children cumulated vsize (Kb) 15112 [startup+250.024 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3632 0 0 0 24925 39 0 0 25 0 1 0 1856027223 13299712 1759 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3247 1759 145 145 0 3102 0 [pid=5782] vsize: 12988 Current children cumulated CPU time (s) 249.65 Current children cumulated vsize (Kb) 15112 [startup+260.024 s] Raw data (loadavg): 1.03 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 3944 0 0 0 25922 41 0 0 25 0 1 0 1856027223 14217216 1829 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3471 1829 145 145 0 3326 0 [pid=5782] vsize: 13884 Current children cumulated CPU time (s) 259.64 Current children cumulated vsize (Kb) 16008 [startup+270.025 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4064 0 0 0 26918 44 0 0 25 0 1 0 1856027223 14794752 1892 4294967295 134512640 135094434 3221224432 3221223320 134795993 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3612 1892 145 145 0 3467 0 [pid=5782] vsize: 14448 Current children cumulated CPU time (s) 269.63 Current children cumulated vsize (Kb) 16572 [startup+280.026 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4184 0 0 0 27916 45 0 0 25 0 1 0 1856027223 15233024 1942 4294967295 134512640 135094434 3221224432 3221223344 134587903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3719 1942 145 145 0 3574 0 [pid=5782] vsize: 14876 Current children cumulated CPU time (s) 279.62 Current children cumulated vsize (Kb) 17000 [startup+290.027 s] Raw data (loadavg): 1.02 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4241 0 0 0 28915 46 0 0 25 0 1 0 1856027223 15564800 1999 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3800 1999 145 145 0 3655 0 [pid=5782] vsize: 15200 Current children cumulated CPU time (s) 289.62 Current children cumulated vsize (Kb) 17324 [startup+300.029 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4347 0 0 0 29913 47 0 0 25 0 1 0 1856027223 16068608 2105 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 3923 2105 145 145 0 3778 0 [pid=5782] vsize: 15692 Current children cumulated CPU time (s) 299.61 Current children cumulated vsize (Kb) 17816 [startup+310.029 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4573 0 0 0 30910 50 0 0 25 0 1 0 1856027223 16793600 2160 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 4100 2160 145 145 0 3955 0 [pid=5782] vsize: 16400 Current children cumulated CPU time (s) 309.61 Current children cumulated vsize (Kb) 18524 [startup+320.03 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4684 0 0 0 31908 51 0 0 25 0 1 0 1856027223 17272832 2271 4294967295 134512640 135094434 3221224432 3221223316 134796009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5782/statm): 4217 2271 145 145 0 4072 0 [pid=5782] vsize: 16868 Current children cumulated CPU time (s) 319.6 Current children cumulated vsize (Kb) 18992 [startup+330.031 s] Raw data (loadavg): 1.01 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4799 0 0 0 32906 51 0 0 25 0 1 0 1856027223 17752064 2322 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5782/statm): 4334 2322 145 145 0 4189 0 [pid=5782] vsize: 17336 Current children cumulated CPU time (s) 329.58 Current children cumulated vsize (Kb) 19460 [startup+340.032 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 4989 0 0 0 33903 54 0 0 25 0 1 0 1856027223 18374656 2366 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5782/statm): 4486 2366 145 145 0 4341 0 [pid=5782] vsize: 17944 Current children cumulated CPU time (s) 339.58 Current children cumulated vsize (Kb) 20068 [startup+350.033 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5177 0 0 0 34900 55 0 0 25 0 1 0 1856027223 18968576 2409 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 4631 2409 145 145 0 4486 0 [pid=5782] vsize: 18524 Current children cumulated CPU time (s) 349.56 Current children cumulated vsize (Kb) 20648 [startup+360.033 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5250 0 0 0 35898 56 0 0 25 0 1 0 1856027223 19292160 2482 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 4710 2482 145 145 0 4565 0 [pid=5782] vsize: 18840 Current children cumulated CPU time (s) 359.55 Current children cumulated vsize (Kb) 20964 [startup+370.034 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5422 0 0 0 36895 57 0 0 25 0 1 0 1856027223 19759104 2518 4294967295 134512640 135094434 3221224432 3221223344 134587868 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5782/statm): 4824 2518 145 145 0 4679 0 [pid=5782] vsize: 19296 Current children cumulated CPU time (s) 369.53 Current children cumulated vsize (Kb) 21420 [startup+380.035 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 5612 0 0 0 37892 59 0 0 25 0 1 0 1856027223 20373504 2584 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5782/statm): 4974 2584 145 145 0 4829 0 [pid=5782] vsize: 19896 Current children cumulated CPU time (s) 379.52 Current children cumulated vsize (Kb) 22020 [startup+390.036 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5735 0 0 0 38890 61 0 0 25 0 1 0 1856027223 20844544 2635 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/5782/statm): 5089 2635 145 145 0 4944 0 [pid=5782] vsize: 20356 Current children cumulated CPU time (s) 389.52 Current children cumulated vsize (Kb) 22480 [startup+400.036 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 5804 0 0 0 39886 62 0 0 25 0 1 0 1856027223 21123072 2704 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 5157 2704 145 145 0 5012 0 [pid=5782] vsize: 20628 Current children cumulated CPU time (s) 399.49 Current children cumulated vsize (Kb) 22752 [startup+410.037 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 8106 0 0 0 40872 70 0 0 25 0 1 0 1856027223 30314496 4580 4294967295 134512640 135094434 3221224432 3221220028 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5782/statm): 7401 4580 145 145 0 7256 0 [pid=5782] vsize: 29604 Current children cumulated CPU time (s) 409.43 Current children cumulated vsize (Kb) 31728 [startup+420.038 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 11052 0 0 0 41857 79 0 0 25 0 1 0 1856027223 41996288 7113 4294967295 134512640 135094434 3221224432 3218839632 134597447 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 10253 7113 145 145 0 10108 0 [pid=5782] vsize: 41012 Current children cumulated CPU time (s) 419.37 Current children cumulated vsize (Kb) 43136 [startup+430.039 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 45064 0 0 0 42658 194 0 0 25 0 1 0 1856027223 138784768 30743 4294967295 134512640 135094434 3221224432 3219105052 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5782/statm): 33883 30743 145 145 0 33738 0 [pid=5782] vsize: 135532 Current children cumulated CPU time (s) 428.53 Current children cumulated vsize (Kb) 137656 [startup+440.04 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 79741 0 0 0 43458 309 0 0 25 0 1 0 1856027223 237625344 54874 4294967295 134512640 135094434 3221224432 3220264768 134594880 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 58014 54874 145 145 0 57869 0 [pid=5782] vsize: 232056 Current children cumulated CPU time (s) 437.68 Current children cumulated vsize (Kb) 234180 [startup+450.04 s] Raw data (loadavg): 1.00 0.99 0.92 2/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) R 5778 5778 19818 0 -1 0 99345 0 0 0 44240 408 0 0 23 0 1 0 1856027223 317923328 74478 4294967295 134512640 135094434 3221224432 3218844624 134594844 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/5782/statm): 77618 74478 145 145 0 77473 0 [pid=5782] vsize: 310472 Current children cumulated CPU time (s) 446.49 Current children cumulated vsize (Kb) 312596 [startup+460.041 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 153807 0 0 0 45009 564 0 0 22 0 1 0 1856027223 454610944 107849 4294967295 134512640 135094434 3221224432 3219613516 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5782/statm): 110989 107849 145 145 0 110844 0 [pid=5782] vsize: 443956 Current children cumulated CPU time (s) 455.74 Current children cumulated vsize (Kb) 446080 [startup+470.042 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 176946 0 0 0 45754 677 0 0 21 0 1 0 1856027223 549388288 130988 4294967295 134512640 135094434 3221224432 3218840172 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5782/statm): 134128 130988 145 145 0 133983 0 [pid=5782] vsize: 536512 Current children cumulated CPU time (s) 464.32 Current children cumulated vsize (Kb) 538636 [startup+480.044 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 200290 0 0 0 46502 786 0 0 22 0 1 0 1856027223 645009408 154332 4294967295 134512640 135094434 3221224432 3218876428 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/5782/statm): 157473 154332 145 145 0 157328 0 [pid=5782] vsize: 629892 Current children cumulated CPU time (s) 472.89 Current children cumulated vsize (Kb) 632016 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+480.471 s] Raw data (loadavg): 1.00 0.99 0.92 1/57 5782 Raw data (/proc/5778/stat): 5778 (minisat+_script) S 5777 5778 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1856027218 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/5778/statm): 531 226 485 147 0 384 0 [pid=5778] vsize: 2124 Raw data (/proc/5782/stat): 5782 (minisat+_64-bit) T 5778 5778 19818 0 -1 0 201286 0 0 0 46534 790 0 0 21 0 1 0 1856027223 994635776 155328 4294967295 134512640 135094434 3221224432 3218861484 134802701 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/5782/statm): 242831 155328 145 145 0 242686 0 [pid=5782] vsize: 971324 Current children cumulated CPU time (s) 473.25 Current children cumulated vsize (Kb) 973448 Sending SIGTERM to -5778 Sleeping 2 seconds One traced child (pid=5778) ended because it received signal 15 (SIGTERM) One traced child (pid=5782) ended because it received signal 11 (SIGSEGV) All traced children have exited ! Game is over. Child ended because it received signal 11 (SIGSEGV) Real time (s): 480.759 CPU time (s): 473.535 CPU user time (s): 465.343 CPU system time (s): 8.19175 CPU usage (%): 98.4975 Max. virtual memory (cumulated for all children) (Kb): 973448
ERROR: no interpretation found !