Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-bf2670-001.opb |
MD5SUM | caacddb078d9307989a3c2624242ecb4 |
Bench Category | optimization, small integers (OPTSMALLINT) |
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 | 2786 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 2786 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 2786 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.132978 |
Number of variables | 2786 |
Total number of constraints | 4827 |
Number of constraints which are clauses | 4827 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 5 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-04 14:55:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=1127 boxname=wulflinc31 idbench=126 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: caacddb078d9307989a3c2624242ecb4 /oldhome/oroussel/tmp/wulflinc31/normalized-bf2670-001.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-bf2670-001.opb IDLAUNCH: 1127 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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.153 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: 907544 kB Buffers: 44348 kB Cached: 60516 kB SwapCached: 944 kB Active: 86352 kB Inactive: 20976 kB HighTotal: 131008 kB HighFree: 69580 kB LowTotal: 903652 kB LowFree: 837964 kB SwapTotal: 2097892 kB SwapFree: 2096432 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5540 kB Slab: 14300 kB Committed_AS: 63656 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-04 14:58:51 (client local time) WITH STATUS 20 IN 194.518 SECONDS stats: 1127 7 194.518 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 2786 variables and 4827 constraints. c After prepocess the problem consists of 712 variables and 1599 constraints. c preprocess terminated 153.221 s c Initial Lower Bound: 1291 c Lower Bound Elapsed time: 0.5513 c Use computed LB before first solution. s UNSATISFIABLE c Exit Code: 20 c Total time: 194.455 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.93 0.97 0.91 2/54 3843 Raw data (stat): 3843 (runsolver) R 3842 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 658283055 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+9.99993 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 18202 0 0 0 953 42 0 0 25 0 1 0 658283055 21032960 4292 4294967295 134512640 134714508 3221221776 3221220352 134535821 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 5135 4292 1111 63 0 5072 0 vsize: 20540 [startup+20.001 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 45190 0 0 0 1889 106 0 0 25 0 1 0 658283055 26791936 5674 4294967295 134512640 134714508 3221221776 3221220392 134543785 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 6541 5674 1111 63 0 6478 0 vsize: 26164 [startup+30.0017 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 52363 0 0 0 2872 123 0 0 25 0 1 0 658283055 29577216 6344 4294967295 134512640 134714508 3221221776 3221220416 134606468 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 7221 6346 1111 63 0 7158 0 vsize: 28884 [startup+40.0016 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 67805 0 0 0 3834 161 0 0 25 0 1 0 658283055 31797248 6907 4294967295 134512640 134714508 3221221776 3221220392 134536921 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 7763 6907 1111 63 0 7700 0 vsize: 31052 [startup+50.0029 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 86597 0 0 0 4791 205 0 0 25 0 1 0 658283055 33796096 7408 4294967295 134512640 134714508 3221221776 3221220140 134539235 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 8251 7408 1111 63 0 8188 0 vsize: 33004 [startup+60.0025 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 100295 0 0 0 5759 237 0 0 25 0 1 0 658283055 34328576 7538 4294967295 134512640 134714508 3221221776 3221220256 134536638 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 8381 7538 1111 63 0 8318 0 vsize: 33524 [startup+70.0034 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 130786 0 0 0 6694 302 0 0 25 0 1 0 658283055 36777984 8136 4294967295 134512640 134714508 3221221776 3221220504 134672913 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 8979 8136 1111 63 0 8916 0 vsize: 35916 [startup+80.0047 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 151668 0 0 0 7642 354 0 0 25 0 1 0 658283055 40595456 9047 4294967295 134512640 134714508 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 9911 9054 1111 63 0 9848 0 vsize: 39644 [startup+90.0043 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 185206 0 0 0 8564 433 0 0 25 0 1 0 658283055 43081728 9675 4294967295 134512640 134714508 3221221776 3221220280 134543609 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 10518 9675 1111 63 0 10455 0 vsize: 42072 [startup+100.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 9562 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220448 134627187 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+110.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 10562 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220448 134627217 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+120.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 11562 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220436 134627197 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 12562 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220448 134627187 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 13562 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220448 134627241 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 186245 0 0 0 14563 435 0 0 25 0 1 0 658283055 45436928 10226 4294967295 134512640 134714508 3221221776 3221220436 134627197 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 11093 10226 1111 63 0 11030 0 vsize: 44372 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 203421 0 0 0 15526 471 0 0 25 0 1 0 658283055 103428096 24116 4294967295 134512640 134714508 3221221776 3221217860 1075964440 0 0 1 0 0 0 0 17 0 0 0 Raw data (statm): 25251 24116 1111 63 0 25188 0 vsize: 101004 [startup+170.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 205149 0 0 0 16521 476 0 0 25 0 1 0 658283055 104366080 24511 4294967295 134512640 134714508 3221221776 3221220176 1074153794 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 25480 24511 1111 63 0 25417 0 vsize: 101920 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 206601 0 0 0 17518 479 0 0 25 0 1 0 658283055 104366080 24511 4294967295 134512640 134714508 3221221776 3221220152 1077410279 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 25480 24511 1111 63 0 25417 0 vsize: 101920 [startup+190.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 207862 0 0 0 18516 481 0 0 25 0 1 0 658283055 105410560 24587 4294967295 134512640 134714508 3221221776 3221217904 1075112100 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 25735 24587 1111 63 0 25672 0 vsize: 102940 [startup+194.547 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 3843 Raw data (stat): 3843 (bsolo_lpr_cuts) R 3842 7876 7672 0 -1 0 207862 0 0 0 18516 481 0 0 25 0 1 0 658283055 105410560 24587 4294967295 134512640 134714508 3221221776 3221217904 1075112100 0 0 1 0 0 0 0 17 1 0 0 Raw data (statm): 25735 24587 1111 63 0 25672 0 vsize: 0 Child status: 20 Real time (s): 194.546 CPU time (s): 194.518 CPU user time (s): 189.641 CPU system time (s): 4.87726 CPU usage (%): 99.9857 Max. virtual memory (Kb): 102940 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####