Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ic97.opb |
MD5SUM | a763f1a89c66e69c15e96e7ec1ddc143 |
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 | 32392558579027 |
Number of bits of the biggest sum of numbers | 45 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 10959 |
Total number of constraints | 10724 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 10588 |
Number of constraints which are nor clauses,nor cardinality constraints | 136 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 9774 |
LAUNCH ON wulflinc13 THE 2005-09-20 05:30:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3481 boxname=wulflinc13 idbench=1137 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a763f1a89c66e69c15e96e7ec1ddc143 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb IDLAUNCH: 3481 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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: 887168 kB Buffers: 32916 kB Cached: 86812 kB SwapCached: 700 kB Active: 49444 kB Inactive: 72948 kB HighTotal: 131008 kB HighFree: 40236 kB LowTotal: 903652 kB LowFree: 846932 kB SwapTotal: 2097136 kB SwapFree: 2095936 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5744 kB Slab: 19376 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 05:34:46 (client local time) WITH STATUS 0 IN 228.193 SECONDS stats: 3481 7 228.193 0
c Parsing PB file... c Converting 932 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################## c -- Clauses(.)/Splits(s): (none) c ---[ 931]---> BDD-cost: 7 c ---[ 930]---> BDD-cost: 8 c ---[ 929]---> BDD-cost: 8 c ---[ 928]---> BDD-cost: 8 c ---[ 927]---> BDD-cost: 7 c ---[ 926]---> BDD-cost: 7 c ---[ 925]---> BDD-cost: 8 c ---[ 924]---> BDD-cost: 7 c ---[ 923]---> BDD-cost: 7 c ---[ 922]---> BDD-cost: 7 c ---[ 921]---> BDD-cost: 7 c ---[ 920]---> BDD-cost: 8 c ---[ 919]---> BDD-cost: 8 c ---[ 918]---> BDD-cost: 7 c ---[ 917]---> BDD-cost: 7 c ---[ 916]---> BDD-cost: 7 c ---[ 915]---> BDD-cost: 7 c ---[ 914]---> BDD-cost: 7 c ---[ 913]---> BDD-cost: 7 c ---[ 912]---> BDD-cost: 7 c ---[ 911]---> BDD-cost: 8 c ---[ 910]---> BDD-cost: 7 c ---[ 909]---> BDD-cost: 7 c ---[ 908]---> BDD-cost: 8 c ---[ 907]---> BDD-cost: 8 c ---[ 906]---> BDD-cost: 8 c ---[ 905]---> BDD-cost: 7 c ---[ 904]---> BDD-cost: 7 c ---[ 903]---> BDD-cost: 8 c ---[ 902]---> BDD-cost: 7 c ---[ 901]---> BDD-cost: 8 c ---[ 900]---> BDD-cost: 8 c ---[ 899]---> BDD-cost: 8 c ---[ 898]---> BDD-cost: 8 c ---[ 897]---> BDD-cost: 8 c ---[ 896]---> BDD-cost: 8 c ---[ 895]---> BDD-cost: 8 c ---[ 894]---> BDD-cost: 8 c ---[ 893]---> BDD-cost: 7 c ---[ 892]---> BDD-cost: 7 c ---[ 891]---> BDD-cost: 7 c ---[ 890]---> BDD-cost: 7 c ---[ 889]---> BDD-cost: 7 c ---[ 888]---> BDD-cost: 8 c ---[ 887]---> BDD-cost: 8 c ---[ 886]---> BDD-cost: 7 c ---[ 885]---> BDD-cost: 7 c ---[ 884]---> BDD-cost: 7 c ---[ 882]---> BDD-cost: 3755 c ---[ 880]---> Adder-cost: 1658 maxlim: 106240 bits: 17/17 c ---[ 878]---> Adder-cost: 2794 maxlim: 179456 bits: 18/18 c ---[ 876]---> Adder-cost: 2732 maxlim: 175360 bits: 18/18 c ---[ 874]---> Adder-cost: 430 maxlim: 28928 bits: 15/15 c ---[ 872]---> Adder-cost: 220 maxlim: 15360 bits: 14/14 c ---[ 870]---> Adder-cost: 4934 maxlim: 340864 bits: 19/19 c ---[ 868]---> Adder-cost: 2686 maxlim: 176768 bits: 18/18 c ---[ 866]---> Adder-cost: 2688 maxlim: 186496 bits: 18/18 c ---[ 864]---> Adder-cost: 1518 maxlim: 142848 bits: 18/18 c ---[ 862]---> Adder-cost: 1392 maxlim: 159616 bits: 18/18 c ---[ 860]---> Adder-cost: 866 maxlim: 56320 bits: 16/16 c ---[ 858]---> Adder-cost: 682 maxlim: 51328 bits: 16/16 c ---[ 856]---> Adder-cost: 374 maxlim: 24448 bits: 15/15 c ---[ 854]---> Adder-cost: 788 maxlim: 62848 bits: 16/16 c ---[ 852]---> Adder-cost: 1240 maxlim: 104320 bits: 17/17 c ---[ 850]---> Adder-cost: 1634 maxlim: 106752 bits: 17/17 c ---[ 848]---> Adder-cost: 652 maxlim: 47232 bits: 16/16 c ---[ 846]---> Adder-cost: 2186 maxlim: 151424 bits: 18/18 c ---[ 844]---> Adder-cost: 620 maxlim: 44288 bits: 16/16 c ---[ 842]---> Adder-cost: 2500 maxlim: 192768 bits: 18/18 c ---[ 840]---> BDD-cost: 2438 c ---[ 838]---> Adder-cost: 172 maxlim: 15360 bits: 14/14 c ---[ 836]---> Adder-cost: 712 maxlim: 56320 bits: 16/16 c ---[ 834]---> Adder-cost: 1206 maxlim: 122880 bits: 17/17 c ---[ 832]---> Adder-cost: 4018 maxlim: 307968 bits: 19/19 c ---[ 830]---> Adder-cost: 1362 maxlim: 105344 bits: 17/17 c ---[ 828]---> BDD-cost: 1898 c ---[ 826]---> Adder-cost: 3290 maxlim: 272768 bits: 19/19 c ---[ 824]---> BDD-cost: 1637 c ---[ 822]---> Adder-cost: 1202 maxlim: 91264 bits: 17/17 c ---[ 820]---> Adder-cost: 1866 maxlim: 156160 bits: 18/18 c ---[ 818]---> Adder-cost: 2840 maxlim: 260864 bits: 18/18 c ---[ 816]---> Adder-cost: 1130 maxlim: 89600 bits: 17/17 c ---[ 814]---> Adder-cost: 604 maxlim: 44672 bits: 16/16 c ---[ 812]---> Adder-cost: 1424 maxlim: 122880 bits: 17/17 c ---[ 810]---> Adder-cost: 456 maxlim: 34688 bits: 16/16 c ---[ 808]---> Adder-cost: 456 maxlim: 34432 bits: 16/16 c ---[ 806]---> BDD-cost: 1595 c ---[ 804]---> BDD-cost:
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/22626/stat): 22626 (minisat+_script) R 22625 22626 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797824647 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/22626/statm): 174 3 169 147 0 27 0 [pid=22626] 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=22627 New process pid=22628 New process pid=22629 execve syscall for /bin/sed executable One traced child (pid=22628) 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=22629) exited with status: 0 One traced child (pid=22627) exited with status: 0 New process pid=22630 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-blp-ic97.opb [startup+10.0039 s] Raw data (loadavg): 0.87 0.94 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 350 0 0 0 988 2 0 0 25 0 1 0 1797824652 1814528 336 4294967295 134512640 135094434 3221224432 3221223300 134796021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 443 336 145 145 0 298 0 [pid=22630] vsize: 1772 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 3896 [startup+20.0046 s] Raw data (loadavg): 0.89 0.94 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 486 0 0 0 1987 3 0 0 25 0 1 0 1797824652 2686976 469 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 656 469 145 145 0 511 0 [pid=22630] vsize: 2624 Current children cumulated CPU time (s) 19.91 Current children cumulated vsize (Kb) 4748 [startup+30.0052 s] Raw data (loadavg): 0.90 0.94 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 602 0 0 0 2984 4 0 0 25 0 1 0 1797824652 3129344 585 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 764 585 145 145 0 619 0 [pid=22630] vsize: 3056 Current children cumulated CPU time (s) 29.89 Current children cumulated vsize (Kb) 5180 [startup+40.0059 s] Raw data (loadavg): 0.92 0.94 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 759 0 0 0 3981 5 0 0 25 0 1 0 1797824652 3698688 670 4294967295 134512640 135094434 3221224432 3221223316 134796021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 903 670 145 145 0 758 0 [pid=22630] vsize: 3612 Current children cumulated CPU time (s) 39.87 Current children cumulated vsize (Kb) 5736 [startup+50.0065 s] Raw data (loadavg): 0.93 0.94 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 894 0 0 0 4978 7 0 0 25 0 1 0 1797824652 4251648 805 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1038 805 145 145 0 893 0 [pid=22630] vsize: 4152 Current children cumulated CPU time (s) 49.86 Current children cumulated vsize (Kb) 6276 [startup+60.0072 s] Raw data (loadavg): 0.94 0.95 0.90 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1092 0 0 0 5974 8 0 0 25 0 1 0 1797824652 5111808 1003 4294967295 134512640 135094434 3221224432 3221223316 134796004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1248 1003 145 145 0 1103 0 [pid=22630] vsize: 4992 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 7116 [startup+70.0079 s] Raw data (loadavg): 0.95 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1336 0 0 0 6970 10 0 0 25 0 1 0 1797824652 6049792 1132 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1477 1132 145 145 0 1332 0 [pid=22630] vsize: 5908 Current children cumulated CPU time (s) 69.81 Current children cumulated vsize (Kb) 8032 [startup+80.0095 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1524 0 0 0 7967 11 0 0 25 0 1 0 1797824652 6848512 1270 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1672 1270 145 145 0 1527 0 [pid=22630] vsize: 6688 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 8812 [startup+90.0102 s] Raw data (loadavg): 0.96 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1761 0 0 0 8963 14 0 0 25 0 1 0 1797824652 7774208 1452 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1898 1452 145 145 0 1753 0 [pid=22630] vsize: 7592 Current children cumulated CPU time (s) 89.78 Current children cumulated vsize (Kb) 9716 [startup+100.011 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 1778 0 0 0 9961 15 0 0 25 0 1 0 1797824652 7864320 1469 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 1920 1469 145 145 0 1775 0 [pid=22630] vsize: 7680 Current children cumulated CPU time (s) 99.77 Current children cumulated vsize (Kb) 9804 [startup+110.012 s] Raw data (loadavg): 0.97 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2076 0 0 0 10957 17 0 0 25 0 1 0 1797824652 9150464 1590 4294967295 134512640 135094434 3221224432 3221223344 134587866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 2234 1590 145 145 0 2089 0 [pid=22630] vsize: 8936 Current children cumulated CPU time (s) 109.75 Current children cumulated vsize (Kb) 11060 [startup+120.013 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2208 0 0 0 11954 19 0 0 25 0 1 0 1797824652 9711616 1653 4294967295 134512640 135094434 3221224432 3221223316 134796014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 2371 1653 145 145 0 2226 0 [pid=22630] vsize: 9484 Current children cumulated CPU time (s) 119.74 Current children cumulated vsize (Kb) 11608 [startup+130.014 s] Raw data (loadavg): 0.98 0.95 0.91 1/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 2381 0 0 0 12951 21 0 0 25 0 1 0 1797824652 10543104 1826 4294967295 134512640 135094434 3221224432 3221223368 134801661 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 2574 1826 145 145 0 2429 0 [pid=22630] vsize: 10296 Current children cumulated CPU time (s) 129.73 Current children cumulated vsize (Kb) 12420 [startup+140.014 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2560 0 0 0 13948 23 0 0 25 0 1 0 1797824652 11235328 1907 4294967295 134512640 135094434 3221224432 3221223316 134795999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 2743 1907 145 145 0 2598 0 [pid=22630] vsize: 10972 Current children cumulated CPU time (s) 139.72 Current children cumulated vsize (Kb) 13096 [startup+150.015 s] Raw data (loadavg): 0.98 0.95 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2698 0 0 0 14946 23 0 0 25 0 1 0 1797824652 11866112 1994 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 2897 1994 145 145 0 2752 0 [pid=22630] vsize: 11588 Current children cumulated CPU time (s) 149.7 Current children cumulated vsize (Kb) 13712 [startup+160.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2897 0 0 0 15943 25 0 0 25 0 1 0 1797824652 12603392 2141 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 3077 2141 145 145 0 2932 0 [pid=22630] vsize: 12308 Current children cumulated CPU time (s) 159.69 Current children cumulated vsize (Kb) 14432 [startup+170.016 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 2995 0 0 0 16939 27 0 0 25 0 1 0 1797824652 13037568 2239 4294967295 134512640 135094434 3221224432 3221223316 134796006 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 3183 2239 145 145 0 3038 0 [pid=22630] vsize: 12732 Current children cumulated CPU time (s) 169.67 Current children cumulated vsize (Kb) 14856 [startup+180.017 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 6182 0 0 0 17923 38 0 0 25 0 1 0 1797824652 23887872 4754 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22630/statm): 5832 4754 145 145 0 5687 0 [pid=22630] vsize: 23328 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 25452 [startup+190.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 42598 0 0 0 18703 169 0 0 20 0 1 0 1797824652 129986560 30663 4294967295 134512640 135094434 3221224432 3220296448 134594941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 31735 30663 145 145 0 31590 0 [pid=22630] vsize: 126940 Current children cumulated CPU time (s) 188.73 Current children cumulated vsize (Kb) 129064 [startup+200.019 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 82011 0 0 0 19453 310 0 0 20 0 1 0 1797824652 248225792 59530 4294967295 134512640 135094434 3221224432 3219763644 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 60602 59530 145 145 0 60457 0 [pid=22630] vsize: 242408 Current children cumulated CPU time (s) 197.64 Current children cumulated vsize (Kb) 244532 [startup+210.02 s] Raw data (loadavg): 0.99 0.96 0.91 2/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) R 22626 22626 1333 0 -1 0 144101 0 0 0 20149 497 0 0 25 0 1 0 1797824652 502546432 121620 4294967295 134512640 135094434 3221224432 3219758528 134597418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22630/statm): 122692 121620 145 145 0 122547 0 [pid=22630] vsize: 490768 Current children cumulated CPU time (s) 206.47 Current children cumulated vsize (Kb) 492892 [startup+220.021 s] Raw data (loadavg): 0.99 0.96 0.91 1/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 161743 0 0 0 20955 588 0 0 20 0 1 0 1797824652 488419328 118171 4294967295 134512640 135094434 3221224432 3219773676 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 119243 118171 145 145 0 119098 0 [pid=22630] vsize: 476972 Current children cumulated CPU time (s) 215.44 Current children cumulated vsize (Kb) 479096 [startup+230.022 s] Raw data (loadavg): 0.99 0.96 0.91 1/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 186307 0 0 0 21690 703 0 0 19 0 1 0 1797824652 589033472 142735 4294967295 134512640 135094434 3221224432 3219755196 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 143807 142735 145 145 0 143662 0 [pid=22630] vsize: 575228 Current children cumulated CPU time (s) 223.94 Current children cumulated vsize (Kb) 577352 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+234.653 s] Raw data (loadavg): 0.99 0.96 0.91 1/57 22630 Raw data (/proc/22626/stat): 22626 (minisat+_script) S 22625 22626 1333 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797824647 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22626/statm): 531 226 485 147 0 384 0 [pid=22626] vsize: 2124 Raw data (/proc/22630/stat): 22630 (minisat+_64-bit) T 22626 22626 1333 0 -1 0 197574 0 0 0 22034 755 0 0 20 0 1 0 1797824652 980733952 154002 4294967295 134512640 135094434 3221224432 3219767004 134802701 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/22630/statm): 239437 154002 145 145 0 239292 0 [pid=22630] vsize: 957748 Current children cumulated CPU time (s) 227.9 Current children cumulated vsize (Kb) 959872 Sending SIGTERM to -22626 Sleeping 2 seconds One traced child (pid=22626) ended because it received signal 15 (SIGTERM) One traced child (pid=22630) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 234.941 CPU time (s): 228.193 CPU user time (s): 220.349 CPU system time (s): 7.84481 CPU usage (%): 97.1279 Max. virtual memory (cumulated for all children) (Kb): 959872
ERROR: no interpretation found !