Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-shell.opb |
MD5SUM | 0f9e797b4b986a37159e9b1332a4b629 |
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 | 39844 |
Biggest coefficient in the objective function | 2101312749568 |
Number of bits for the biggest coefficient in the objective function | 41 |
Sum of the numbers in the objective function | 249967315526150 |
Number of bits of the sum of numbers in the objective function | 48 |
Biggest number in a constraint | 2101312749568 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 249967315526150 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 45231 |
Total number of constraints | 653 |
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 | 653 |
Minimum length of a constraint | 19 |
Maximum length of a constraint | 1560 |
LAUNCH ON wulflinc24 THE 2005-09-18 20:35:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2815 boxname=wulflinc24 idbench=471 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 0f9e797b4b986a37159e9b1332a4b629 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-shell.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-shell.opb IDLAUNCH: 2815 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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 : 3 cpu MHz : 451.080 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: 911028 kB Buffers: 35112 kB Cached: 60500 kB SwapCached: 744 kB Active: 70016 kB Inactive: 28264 kB HighTotal: 131008 kB HighFree: 67312 kB LowTotal: 903652 kB LowFree: 843716 kB SwapTotal: 2097892 kB SwapFree: 2096644 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 19672 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 20:36:04 (client local time) WITH STATUS 139 IN 9.8715 SECONDS stats: 2815 7 9.8715 139
c Parsing PB file... c Converting 1187 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ##################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): ssssssssss c ---[1195]---> BDD-cost: 26 c ---[1194]---> BDD-cost: 26 c ---[1193]---> BDD-cost: 24 c ---[1191]---> BDD-cost: 25 c ---[1187]---> BDD-cost: 27 c ---[1185]---> BDD-cost: 26 c ---[1183]---> BDD-cost: 26 c ---[1182]---> BDD-cost: 26 c ---[1181]---> BDD-cost: 26 c ---[1180]---> BDD-cost: 26 c ---[1179]---> BDD-cost: 26 c ---[1178]---> BDD-cost: 26 c ---[1177]---> BDD-cost: 26 c ---[1176]---> BDD-cost: 26 c ---[1175]---> BDD-cost: 26 c ---[1174]---> BDD-cost: 26 c ---[1173]---> BDD-cost: 26 c ---[1172]---> BDD-cost: 26 c ---[1171]---> BDD-cost: 26 c ---[1170]---> BDD-cost: 26 c ---[1169]---> BDD-cost: 26 c ---[1168]---> BDD-cost: 26 c ---[1167]---> BDD-cost: 26 c ---[1166]---> BDD-cost: 26 c ---[1165]---> BDD-cost: 26 c ---[1164]---> BDD-cost: 26 c ---[1163]---> BDD-cost: 26 c ---[1162]---> BDD-cost: 26 c ---[1161]---> BDD-cost: 26 c ---[1160]---> BDD-cost: 26 c ---[1159]---> BDD-cost: 26 c ---[1158]---> BDD-cost: 26 c ---[1157]---> BDD-cost: 26 c ---[1156]---> BDD-cost: 26 c ---[1155]---> BDD-cost: 26 c ---[1154]---> BDD-cost: 26 c ---[1153]---> BDD-cost: 26 c ---[1152]---> BDD-cost: 26 c ---[1151]---> BDD-cost: 26 c ---[1150]---> BDD-cost: 25 c ---[1149]---> BDD-cost: 26 c ---[1147]---> BDD-cost: 22 c ---[1146]---> BDD-cost: 22 c ---[1145]---> BDD-cost: 26 c ---[1143]---> BDD-cost: 23 c ---[1142]---> BDD-cost: 23 c ---[1141]---> BDD-cost: 23 c ---[1140]---> BDD-cost: 21 c ---[1139]---> BDD-cost: 23 c ---[1138]---> BDD-cost: 24 c ---[1137]---> BDD-cost: 26 c ---[1136]---> BDD-cost: 26 c ---[1135]---> BDD-cost: 26 c ---[1134]---> BDD-cost: 26 c ---[1133]---> BDD-cost: 26 c ---[1131]---> BDD-cost: 21 c ---[1130]---> BDD-cost: 24 c ---[1129]---> BDD-cost: 26 c ---[1128]---> BDD-cost: 26 c ---[1127]---> BDD-cost: 26 c ---[1126]---> BDD-cost: 23 c ---[1125]---> BDD-cost: 26 c ---[1124]---> BDD-cost: 22 c ---[1122]---> BDD-cost: 26 c ---[1120]---> BDD-cost: 22 c ---[1119]---> BDD-cost: 21 c ---[1116]---> BDD-cost: 23 c ---[1115]---> BDD-cost: 23 c ---[1114]---> BDD-cost: 26 c ---[1113]---> BDD-cost: 26 c ---[1112]---> BDD-cost: 26 c ---[1111]---> BDD-cost: 26 c ---[1110]---> BDD-cost: 26 c ---[1107]---> BDD-cost: 23 c ---[1106]---> BDD-cost: 26 c ---[1105]---> BDD-cost: 26 c ---[1104]---> BDD-cost: 26 c ---[1103]---> BDD-cost: 22 c ---[1102]---> BDD-cost: 26 c ---[1101]---> BDD-cost: 21 c ---[1100]---> BDD-cost: 20 c ---[1099]---> BDD-cost: 19 c ---[1098]---> BDD-cost: 26 c ---[1096]---> BDD-cost: 20 c ---[1093]---> BDD-cost: 22 c ---[1092]---> BDD-cost: 19 c ---[1091]---> BDD-cost: 21 c ---[1090]---> BDD-cost: 26 c ---[1089]---> BDD-cost: 26 c ---[1088]---> BDD-cost: 26 c ---[1087]---> BDD-cost: 26 c ---[1086]---> BDD-cost: 26 c ---[1084]---> BDD-cost: 22 c ---[1083]---> BDD-cost: 18 c ---[1082]---> BDD-cost: 26 c ---[1081]---> BDD-cost: 26 c ---[1080]---> BDD-cost: 26 c ---[1079]---> Sorter-cost: 571 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[107/oldhome/oroussel/solvers/minisat+_script: line 9: 27109 Segmentation fault $XDIR/minisat+_64-bit_static -try "$@"
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/27105/stat): 27105 (minisat+_script) R 27104 27105 20728 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1844181849 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27105/statm): 174 3 169 147 0 27 0 [pid=27105] 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=27106 New process pid=27107 New process pid=27108 execve syscall for /bin/sed executable One traced child (pid=27107) 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=27108) exited with status: 0 One traced child (pid=27106) exited with status: 0 New process pid=27109 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-shell.opb [startup+10.0038 s] Raw data (loadavg): 0.93 0.96 0.94 2/57 27109 Raw data (/proc/27105/stat): 27105 (minisat+_script) S 27104 27105 20728 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1844181849 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/27105/statm): 531 226 485 147 0 384 0 [pid=27105] vsize: 2124 Raw data (/proc/27109/stat): 27109 (minisat+_64-bit) R 27105 27105 20728 0 -1 1028 135458 0 0 0 635 342 0 0 25 0 1 0 1844181854 0 0 4294967295 0 0 0 0 0 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27109/statm): 0 0 0 0 0 0 0 [pid=27109] vsize: 0 Current children cumulated CPU time (s) 9.77 Current children cumulated vsize (Kb) 2124 One traced child (pid=27109) ended because it received signal 11 (SIGSEGV) One traced child (pid=27105) exited with status: 139 All traced children have exited ! Game is over. Child status: 139 Real time (s): 10.0775 CPU time (s): 9.8715 CPU user time (s): 6.36303 CPU system time (s): 3.50847 CPU usage (%): 97.9563 Max. virtual memory (cumulated for all children) (Kb): 2124
ERROR: no interpretation found !