Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-van.opb |
MD5SUM | 63aca17b11625a83c7613ee93b3a2e23 |
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 | 192 |
Biggest coefficient in the objective function | 2427002644 |
Number of bits for the biggest coefficient in the objective function | 32 |
Sum of the numbers in the objective function | 319999999936 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 28349428224 |
Number of bits of the biggest number in a constraint | 35 |
Biggest sum of numbers in a constraint | 319999999936 |
Number of bits of the biggest sum of numbers | 39 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 139.971 |
Number of variables | 98496 |
Total number of constraints | 39811 |
Number of constraints which are clauses | 128 |
Number of constraints which are cardinality constraints (but not clauses) | 195 |
Number of constraints which are nor clauses,nor cardinality constraints | 39488 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 361 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc1 THE 2005-04-20 23:13:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=20338 boxname=wulflinc1 idbench=1565 idsolver=6 numberseed=0 MD5SUM SOLVER: 2225cba0d9b2c30e235f6cafc823d7ac /oldhome/oroussel/solvers/PBS4 MD5SUM BENCH: 63aca17b11625a83c7613ee93b3a2e23 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-van.opb REAL COMMAND: PBS4 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-van.opb IDLAUNCH: 20338 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.053 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.053 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: 559764 kB Buffers: 20892 kB Cached: 426004 kB SwapCached: 0 kB Active: 210528 kB Inactive: 239516 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 559512 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 32 kB Writeback: 0 kB Mapped: 7220 kB Slab: 18904 kB Committed_AS: 92820 kB PageTables: 344 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-20 23:16:21 (client local time) WITH STATUS 20 IN 139.971 SECONDS stats: 20338 7 139.971 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c PBS v4 by Bashar Al-Rawi & Fadi Aloul c Solving /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-van.opb ...... s UNSATISFIABLE c Done, CPU Time=0.280957 #### 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): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (runsolver) R 15817 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 425237487 1052672 99 4294967295 134512640 135381576 3221224528 3221219776 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+9.99961 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 6668 0 0 0 977 22 0 0 25 0 1 0 425237487 27967488 6408 4294967295 134512640 135450300 3221224640 3221157392 134863903 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6828 6408 231 231 0 6597 0 vsize: 27312 [startup+20.0004 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 8103 0 0 0 1969 30 0 0 25 0 1 0 425237487 34058240 7843 4294967295 134512640 135450300 3221224640 3221157568 134846922 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8315 7843 231 231 0 8084 0 vsize: 33260 [startup+30.0001 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 9440 0 0 0 2959 40 0 0 25 0 1 0 425237487 39145472 9180 4294967295 134512640 135450300 3221224640 3221157376 134855169 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9557 9180 231 231 0 9326 0 vsize: 38228 [startup+39.9999 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 10855 0 0 0 3949 50 0 0 25 0 1 0 425237487 45387776 10595 4294967295 134512640 135450300 3221224640 3221157440 134598676 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11081 10595 231 231 0 10850 0 vsize: 44324 [startup+50.0197 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 12171 0 0 0 4942 59 0 0 25 0 1 0 425237487 49889280 11911 4294967295 134512640 135450300 3221224640 3221157376 134855169 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12180 11911 231 231 0 11949 0 vsize: 48720 [startup+60.02 s] Raw data (loadavg): 1.00 0.96 0.91 2/56 15818 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 17154 0 0 0 5925 76 0 0 25 0 1 0 425237487 71462912 16685 4294967295 134512640 135450300 3221224640 3221157440 134599693 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17447 16685 231 231 0 17216 0 vsize: 69788 [startup+70.0203 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 17164 0 0 0 6919 83 0 0 25 0 1 0 425237487 71462912 16695 4294967295 134512640 135450300 3221224640 3221157504 134515788 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17447 16695 231 231 0 17216 0 vsize: 69788 [startup+80.0211 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 17174 0 0 0 7912 89 0 0 25 0 1 0 425237487 71462912 16705 4294967295 134512640 135450300 3221224640 3221157360 134523757 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17447 16705 231 231 0 17216 0 vsize: 69788 [startup+90.0208 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 18245 0 0 0 8904 97 0 0 25 0 1 0 425237487 75788288 17776 4294967295 134512640 135450300 3221224640 3221157440 134598590 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 18503 17776 231 231 0 18272 0 vsize: 74012 [startup+100.021 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 19386 0 0 0 9898 104 0 0 25 0 1 0 425237487 80388096 18917 4294967295 134512640 135450300 3221224640 3221157236 134524043 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 19626 18917 231 231 0 19395 0 vsize: 78504 [startup+110.026 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 20525 0 0 0 10889 114 0 0 25 0 1 0 425237487 84987904 20056 4294967295 134512640 135450300 3221224640 3221157600 134674684 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 20749 20056 231 231 0 20518 0 vsize: 82996 [startup+120.028 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 21645 0 0 0 11881 122 0 0 25 0 1 0 425237487 89448448 21176 4294967295 134512640 135450300 3221224640 3221157376 134855106 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21838 21176 231 231 0 21607 0 vsize: 87352 [startup+130.028 s] Raw data (loadavg): 1.00 0.97 0.91 2/56 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 22790 0 0 0 12872 131 0 0 25 0 1 0 425237487 94044160 22321 4294967295 134512640 135450300 3221224640 3221157360 134523701 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 22960 22321 231 231 0 22729 0 vsize: 91840 [startup+139.958 s] Raw data (loadavg): 1.00 0.97 0.91 1/55 15820 Raw data (stat): 15818 (PBS4) R 15817 12452 12451 0 -1 0 22790 0 0 0 12872 131 0 0 25 0 1 0 425237487 94044160 22321 4294967295 134512640 135450300 3221224640 3221157360 134523701 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 22960 22321 231 231 0 22729 0 vsize: 0 Child status: 20 Real time (s): 139.958 CPU time (s): 139.971 CPU user time (s): 138.311 CPU system time (s): 1.65975 CPU usage (%): 100.009 Max. virtual memory (Kb): 91840 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####