Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gesa3_o.opb |
MD5SUM | fca009b84c2f2c99c6eab1b54cde16f4 |
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 | 6144 |
Biggest coefficient in the objective function | 409031671808 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 143020903040784 |
Number of bits of the sum of numbers in the objective function | 48 |
Biggest number in a constraint | 524288000000 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 143020903040784 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.099984 |
Number of variables | 10704 |
Total number of constraints | 1560 |
Number of constraints which are clauses | 168 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1392 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 211 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc29 THE 2005-05-28 13:37:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=24946 boxname=wulflinc29 idbench=1418 idsolver=17 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: fca009b84c2f2c99c6eab1b54cde16f4 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-gesa3_o.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-gesa3_o.opb IDLAUNCH: 24946 /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: 709056 kB Buffers: 34884 kB Cached: 265656 kB SwapCached: 632 kB Active: 17548 kB Inactive: 285084 kB HighTotal: 131008 kB HighFree: 1540 kB LowTotal: 903652 kB LowFree: 707516 kB SwapTotal: 2097892 kB SwapFree: 2096368 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5132 kB Slab: 17252 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-28 13:39:14 (client local time) WITH STATUS 1 IN 100.617 SECONDS stats: 24946 7 100.617 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.87 0.93 0.90 2/54 29957 Raw data (stat): 29957 (runsolver) R 29956 20001 20000 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 865214205 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.001 s] Raw data (loadavg): 0.89 0.93 0.90 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 29373 0 0 0 938 61 0 0 25 0 1 0 865214205 92094464 18226 4294967295 134512640 135726644 3221224576 3218778720 134604405 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 22484 18226 300 300 0 22184 0 vsize: 89936 [startup+20.0014 s] Raw data (loadavg): 0.91 0.93 0.90 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 59225 0 0 0 1878 121 0 0 25 0 1 0 865214205 180781056 36834 4294967295 134512640 135726644 3221224576 3218799728 134554559 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 44136 36834 300 300 0 43836 0 vsize: 176544 [startup+30.0022 s] Raw data (loadavg): 0.92 0.93 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 98197 0 0 0 2796 203 0 0 25 0 1 0 865214205 296194048 53585 4294967295 134512640 135726644 3221224576 3218767412 135280408 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 72313 53585 300 300 0 72013 0 vsize: 289252 [startup+40.0033 s] Raw data (loadavg): 0.93 0.93 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 117756 0 0 0 3758 241 0 0 25 0 1 0 865214205 355971072 72894 4294967295 134512640 135726644 3221224576 3218798400 135105730 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 86907 72894 300 300 0 86607 0 vsize: 347628 [startup+50.0037 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 158630 0 0 0 4679 320 0 0 25 0 1 0 865214205 487993344 94154 4294967295 134512640 135726644 3221224576 3218762232 135280592 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 119139 94154 300 300 0 118839 0 vsize: 476556 [startup+60.0035 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 195166 0 0 0 5603 397 0 0 25 0 1 0 865214205 588656640 105883 4294967295 134512640 135726644 3221224576 3218752064 134767064 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 143715 105884 300 300 0 143415 0 vsize: 574860 [startup+70.0065 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 211110 0 0 0 6570 430 0 0 25 0 1 0 865214205 638025728 121599 4294967295 134512640 135726644 3221224576 3218760064 134767123 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 155768 121600 300 300 0 155468 0 vsize: 623072 [startup+80.0069 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 232401 0 0 0 7526 475 0 0 25 0 1 0 865214205 669790208 142627 4294967295 134512640 135726644 3221224576 3218752080 134782642 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 163523 142628 300 300 0 163223 0 vsize: 654092 [startup+90.0078 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 253471 0 0 0 8482 519 0 0 25 0 1 0 865214205 703471616 163440 4294967295 134512640 135726644 3221224576 3218758064 134767052 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 171746 163440 300 300 0 171446 0 vsize: 686984 [startup+100.008 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 253747 0 0 0 9468 533 0 0 25 0 1 0 865214205 394399744 95313 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 96289 95313 300 300 0 95989 0 vsize: 385156 [startup+100.614 s] Raw data (loadavg): 0.97 0.94 0.91 1/53 29957 Raw data (stat): 29957 (pb2sat) R 29956 20001 20000 0 -1 0 253747 0 0 0 9468 533 0 0 25 0 1 0 865214205 394399744 95313 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 96289 95313 300 300 0 95989 0 vsize: 0 Child status: 1 Real time (s): 100.614 CPU time (s): 100.617 CPU user time (s): 95.0855 CPU system time (s): 5.53116 CPU usage (%): 100.003 Max. virtual memory (Kb): 686984 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####