| Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-d2q06c.opb |
| MD5SUM | 91ef78d459f6272891a68c3f1abe1bde |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | NO |
| (Un)Satisfiability was proved | |
| Best value of the objective function | |
| Optimality of the best value was proved | |
| Number of terms in the objective function | 89670 |
| Biggest coefficient in the objective function | 36281708852543488 |
| Number of bits for the biggest coefficient in the objective function | 56 |
| Sum of the numbers in the objective function | -1012211575040220109 |
| Number of bits of the sum of numbers in the objective function | 64 |
| Biggest number in a constraint | 1246989811751845888 |
| Number of bits of the biggest number in a constraint | 61 |
| Biggest sum of numbers in a constraint | -1012211575040220109 |
| Number of bits of the biggest sum of numbers | 64 |
| Best result obtained on this benchmark | UNSAT |
| Best CPU time to get the best result obtained on this benchmark | 92.5719 |
| Number of variables | 155010 |
| Total number of constraints | 2171 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 0 |
| Number of constraints which are nor clauses,nor cardinality constraints | 2171 |
| Minimum length of a constraint | 30 |
| Maximum length of a constraint | 3270 |
LAUNCH ON wulflinc15 THE 2005-09-19 00:08:32 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=6280 boxname=wulflinc15 idbench=420 idsolver=6 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 91ef78d459f6272891a68c3f1abe1bde /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-d2q06c.opb REAL COMMAND: java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoTer.jar /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-d2q06c.opb IDLAUNCH: 6280 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 450.999 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: 876688 kB Buffers: 34044 kB Cached: 94260 kB SwapCached: 692 kB Active: 88348 kB Inactive: 42612 kB HighTotal: 131008 kB HighFree: 33572 kB LowTotal: 903652 kB LowFree: 843116 kB SwapTotal: 2097136 kB SwapFree: 2095920 kB Dirty: 44 kB Writeback: 0 kB Mapped: 5732 kB Slab: 21236 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-19 00:09:59 (client local time) WITH STATUS 20 IN 92.5719 SECONDS stats: 6280 7 92.5719 20
c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre c This is free software under the GNU LGPL licence. See www.sat4j.org for details. c version JAVA5.1.1.31 c --- Begin Solver configuration --- c org.sat4j.minisat.uip.FirstUIP@a20892 c org.sat4j.minisat.constraints.PBMinDataStructure@1e0bc08 c org.sat4j.minisat.learning.MiniSATLearning@158b649 c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 c VSIDS like heuristics from MiniSAT using a sorted array c No reason simplification c --- End Solver configuration --- c solving /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-d2q06c.opb c reading problem ... done. Time 46.082 ms. c #vars 155010 c #constraints 3674 c starts : 0 c conflicts : 0 c decisions : 0 c propagations : 48502 c inspects : 19450 c learnt literals : 0 c learnt binary clauses : 0 c learnt ternary clauses : 0 c learnt clauses : 0 c root simplifications : 0 c removed literals (reason simplification) : 0 c reason swapping (by a shorter reason) : 0 c Calls to reduceDB : 0 c speed (decisions/second) : 0.0 c non guided choices 0 c random choices 0 s UNSATISFIABLE c Total CPU time (ms) : 85.264
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/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1787220141 159744 3 4294967295 134512640 134569956 3221224464 3221224464 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/13671/statm): 39 3 38 16 0 23 0
[pid=13671] vsize: 156
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libpthread.so.0
open syscall for file tls/i686/libpthread.so.0
open syscall for file tls/mmx/libpthread.so.0
open syscall for file tls/libpthread.so.0
open syscall for file i686/mmx/libpthread.so.0
open syscall for file i686/libpthread.so.0
open syscall for file mmx/libpthread.so.0
open syscall for file libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/libpthread.so.0
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libpthread.so.0
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 /oldhome/oroussel/solvers/sat4jPseudoTer.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/jvm.cfg
execve syscall for /oldhome/oroussel/jre1.5.0_05/bin/java executable
open syscall for file /etc/ld.so.preload
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/tls/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/tls/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/tls/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/tls/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/tls/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/tls/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/tls/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/tls/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/tls/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/../lib/i386/libpthread.so.0
open syscall for file tls/i686/mmx/libpthread.so.0
open syscall for file tls/i686/libpthread.so.0
open syscall for file tls/mmx/libpthread.so.0
open syscall for file tls/libpthread.so.0
open syscall for file i686/mmx/libpthread.so.0
open syscall for file i686/libpthread.so.0
open syscall for file mmx/libpthread.so.0
open syscall for file libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/i686/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/i686/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/mmx/libpthread.so.0
open syscall for file /oldhome/oroussel/lib/libpthread.so.0
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libpthread.so.0
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libdl.so.2
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libdl.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 /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libc.so.6
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libc.so.6
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 /oldhome/oroussel/solvers/sat4jPseudoTer.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/jvm.cfg
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libjvm.so
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libm.so.6
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libm.so.6
open syscall for file tls/i686/mmx/libm.so.6
open syscall for file tls/i686/libm.so.6
open syscall for file tls/mmx/libm.so.6
open syscall for file tls/libm.so.6
open syscall for file i686/mmx/libm.so.6
open syscall for file i686/libm.so.6
open syscall for file mmx/libm.so.6
open syscall for file libm.so.6
open syscall for file /oldhome/oroussel/lib/libm.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libm.so.6
open syscall for file /etc/mtab
open syscall for file /proc/stat
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file .hotspotrc
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/endorsed
open syscall for file /etc/mtab
open syscall for file /proc/stat
open syscall for file /proc/self/maps
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/native_threads/libhpi.so
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/libnsl.so.1
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libnsl.so.1
open syscall for file tls/i686/mmx/libnsl.so.1
open syscall for file tls/i686/libnsl.so.1
open syscall for file tls/mmx/libnsl.so.1
open syscall for file tls/libnsl.so.1
open syscall for file i686/mmx/libnsl.so.1
open syscall for file i686/libnsl.so.1
open syscall for file mmx/libnsl.so.1
open syscall for file libnsl.so.1
open syscall for file /oldhome/oroussel/lib/libnsl.so.1
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libnsl.so.1
socket syscall socket(PF_UNIX,SOCK_STREAM,0)=4
socket syscall connect(4,{sa_family=AF_UNIX,path=/var/run/.nscd_socket},110)
open syscall for file /tmp/hsperfdata_oroussel
open syscall for file /tmp/hsperfdata_oroussel/13671
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libverify.so
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libjava.so
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/libzip.so
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/rt.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/jsse.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/jce.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/charsets.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/i386/server/classes.jsa
open syscall for file .hotspot_compiler
New thread pid=13672
New thread pid=13673
New thread pid=13674
socket syscall socket(PF_UNIX,SOCK_STREAM,0)=4
socket syscall connect(4,{sa_family=AF_UNIX,path=/var/run/.nscd_socket},110)
open syscall for file /etc/localtime
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/ext
New thread pid=13675
New thread pid=13676
New thread pid=13677
New thread pid=13678
New thread pid=13679
New thread pid=13680
open syscall for file /oldhome/oroussel/solvers/sat4jPseudoTer.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/ext/sunjce_provider.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/ext/sunpkcs11.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/ext/dnsns.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/ext/localedata.jar
open syscall for file /oldhome/oroussel/jre1.5.0_05/lib/security/java.security
open syscall for file /dev/random
open syscall for file /dev/urandom
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-20-10-d2q06c.opb
[startup+10.0024 s]
Raw data (loadavg): 1.19 1.04 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18093 0 1 0 632 49 0 0 19 0 10 0 1787220141 857931776 26751 4294967295 134512640 134569956 3221224336 3221213920 1131371830 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209456 26751 13129 16 0 209440 0
[pid=13671] vsize: 837824
Current children cumulated CPU time (s) 6.81
Current children cumulated vsize (Kb) 837824
[startup+20.0042 s]
Raw data (loadavg): 1.16 1.04 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) S 13670 13671 31778 0 -1 0 18097 0 1 0 1459 55 0 0 25 0 10 0 1787220141 856739840 34913 4294967295 134512640 134569956 3221224336 3221213000 1073952481 0 4 1 23758 0 0 0 17 0 0 0
Raw data (/proc/13671/statm): 209165 34915 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 15.14
Current children cumulated vsize (Kb) 836660
[startup+30.005 s]
Raw data (loadavg): 1.13 1.04 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18099 0 1 0 2278 63 0 0 25 0 10 0 1787220141 856739840 43107 4294967295 134512640 134569956 3221224336 3221213992 1131482272 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209165 43107 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 23.41
Current children cumulated vsize (Kb) 836660
[startup+40.0058 s]
Raw data (loadavg): 1.11 1.03 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18103 0 1 0 3071 70 0 0 25 0 10 0 1787220141 856739840 51589 4294967295 134512640 134569956 3221224336 3221214728 1131333081 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209165 51589 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 31.41
Current children cumulated vsize (Kb) 836660
[startup+50.0067 s]
Raw data (loadavg): 1.17 1.05 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18154 0 1 0 3822 75 0 0 16 0 10 0 1787220141 856739840 62262 4294967295 134512640 134569956 3221224336 3221214680 1131591954 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209165 62262 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 38.97
Current children cumulated vsize (Kb) 836660
[startup+60.0065 s]
Raw data (loadavg): 1.14 1.05 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18165 0 1 0 4721 76 0 0 16 0 10 0 1787220141 856739840 63044 4294967295 134512640 134569956 3221224336 3221214664 1131592037 0 4 1 23758 0 0 0 17 0 0 0
Raw data (/proc/13671/statm): 209165 63044 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 47.97
Current children cumulated vsize (Kb) 836660
[startup+70.0073 s]
Raw data (loadavg): 1.12 1.04 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18176 0 1 0 5609 76 0 0 16 0 10 0 1787220141 856739840 63044 4294967295 134512640 134569956 3221224336 3221214664 1131594015 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209165 63044 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 56.85
Current children cumulated vsize (Kb) 836660
[startup+80.0081 s]
Raw data (loadavg): 1.10 1.04 1.01 2/65 13680
Raw data (/proc/13671/stat): 13671 (java) R 13670 13671 31778 0 -1 0 18186 0 1 0 6485 76 0 0 16 0 10 0 1787220141 856739840 63091 4294967295 134512640 134569956 3221224336 3221214576 1131536972 0 4 1 23758 0 0 0 17 1 0 0
Raw data (/proc/13671/statm): 209165 63091 13129 16 0 209149 0
[pid=13671] vsize: 836660
Current children cumulated CPU time (s) 65.61
Current children cumulated vsize (Kb) 836660
New thread pid=13681
One traced child (pid=13681) exited with status: 0
One traced child (pid=13680) exited with status: 0
One traced child (pid=13675) exited with status: 0
One traced child (pid=13672) exited with status: 20
One traced child (pid=13679) exited with status: 20
One traced child (pid=13673) exited with status: 20
One traced child (pid=13674) exited with status: 20
One traced child (pid=13676) exited with status: 20
One traced child (pid=13677) exited with status: 20
One traced child (pid=13678) exited with status: 20
One traced child (pid=13671) exited with status: 20
All traced children have exited ! Game is over.
Child status: 20
Real time (s): 86.7052
CPU time (s): 92.5719
CPU user time (s): 90.6272
CPU system time (s): 1.9447
CPU usage (%): 106.766
Max. virtual memory (cumulated for all children) (Kb): 837824
ERROR: no interpretation found !