Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-CMS750_4.opb |
MD5SUM | 7cb58e3aea22e107ecbc4e74969c24f1 |
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 | 780 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 1074509823 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 1024000000 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 2147731454 |
Number of bits of the biggest sum of numbers | 32 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 22.6916 |
Number of variables | 142226 |
Total number of constraints | 28077 |
Number of constraints which are clauses | 2438 |
Number of constraints which are cardinality constraints (but not clauses) | 7196 |
Number of constraints which are nor clauses,nor cardinality constraints | 18443 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 61 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-05-24 14:36:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15004 boxname=wulflinc8 idbench=1155 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 7cb58e3aea22e107ecbc4e74969c24f1 /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-CMS750_4.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-CMS750_4.opb IDLAUNCH: 15004 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 925796 kB Buffers: 34292 kB Cached: 53088 kB SwapCached: 0 kB Active: 66968 kB Inactive: 23452 kB HighTotal: 131008 kB HighFree: 73584 kB LowTotal: 903652 kB LowFree: 852212 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 4 kB Writeback: 0 kB Mapped: 7064 kB Slab: 12792 kB Committed_AS: 63736 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-24 14:37:29 (client local time) WITH STATUS 20 IN 80.8257 SECONDS stats: 15004 7 80.8257 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 142226 variables and 20882 constraints. s UNSATISFIABLE c Exit Code: 20 c Total time: 80.554 s #### 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 Raw data (loadavg): 0.72 1.25 1.79 2/54 3176 Raw data (stat): 3176 (runsolver) R 3175 3132 3131 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 759218201 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0078 s] Raw data (loadavg): 0.76 1.25 1.78 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 45248 0 8 0 725 103 0 0 25 0 1 0 759218201 197931008 44877 4294967295 134512640 134714508 3221224576 3221221052 1077191619 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 48323 44877 1111 63 0 48260 0 vsize: 193292 [startup+20.203 s] Raw data (loadavg): 0.80 1.24 1.77 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 85623 0 8 0 1657 191 0 0 25 0 1 0 759218201 360636416 84406 4294967295 134512640 134714508 3221224576 3221223112 134543609 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 88046 84407 1111 63 0 87983 0 vsize: 352184 [startup+30.21 s] Raw data (loadavg): 0.83 1.23 1.76 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 102002 0 8 0 2625 223 0 0 25 0 1 0 759218201 427671552 100785 4294967295 134512640 134714508 3221224576 3221222860 1077399562 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 104412 100785 1111 63 0 104349 0 vsize: 417648 [startup+40.2102 s] Raw data (loadavg): 0.85 1.22 1.75 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 119084 0 8 0 3592 256 0 0 25 0 1 0 759218201 497655808 117867 4294967295 134512640 134714508 3221224576 3221222860 1077399562 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 121498 117867 1111 63 0 121435 0 vsize: 485992 [startup+50.2114 s] Raw data (loadavg): 0.87 1.21 1.74 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 124593 0 8 0 4581 268 0 0 25 0 1 0 759218201 520187904 123376 4294967295 134512640 134714508 3221224576 3221222236 1077244416 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 126999 123376 1111 63 0 126936 0 vsize: 507996 [startup+60.2124 s] Raw data (loadavg): 0.89 1.21 1.74 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 127045 0 8 0 5574 274 0 0 25 0 1 0 759218201 530190336 125828 4294967295 134512640 134714508 3221224576 3221222860 1077399552 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 129441 125828 1111 63 0 129378 0 vsize: 517764 [startup+70.2127 s] Raw data (loadavg): 0.91 1.20 1.73 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 129968 0 8 0 6567 282 0 0 25 0 1 0 759218201 542220288 128751 4294967295 134512640 134714508 3221224576 3221222864 134566780 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 132378 128751 1111 63 0 132315 0 vsize: 529512 [startup+80.2299 s] Raw data (loadavg): 0.92 1.19 1.72 2/54 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 132793 0 8 0 7561 289 0 0 25 0 1 0 759218201 553844736 131576 4294967295 134512640 134714508 3221224576 3221223224 134569039 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 135216 131576 1111 63 0 135153 0 vsize: 540864 [startup+82.55 s] Raw data (loadavg): 0.92 1.19 1.72 1/53 3176 Raw data (stat): 3176 (bsolo_lpr_cuts) R 3175 3132 3131 0 -1 0 132793 0 8 0 7561 289 0 0 25 0 1 0 759218201 553844736 131576 4294967295 134512640 134714508 3221224576 3221223224 134569039 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 135216 131576 1111 63 0 135153 0 vsize: 0 Child status: 20 Real time (s): 82.5496 CPU time (s): 80.8257 CPU user time (s): 77.4132 CPU system time (s): 3.41248 CPU usage (%): 97.9117 Max. virtual memory (Kb): 540864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####