Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos4.opb |
MD5SUM | e465af1c9ec9e748a7782ddbee36d3b1 |
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 | 100590 |
Biggest coefficient in the objective function | 11202704073084108800000000 |
Number of bits for the biggest coefficient in the objective function | 84 |
Sum of the numbers in the objective function | 2862789126208280618841669632 |
Number of bits of the sum of numbers in the objective function | 92 |
Biggest number in a constraint | 11202704073084108800000000 |
Number of bits of the biggest number in a constraint | 84 |
Biggest sum of numbers in a constraint | 2862789126208280618841669632 |
Number of bits of the biggest sum of numbers | 92 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 1.90971 |
Number of variables | 203044 |
Total number of constraints | 56505 |
Number of constraints which are clauses | 32142 |
Number of constraints which are cardinality constraints (but not clauses) | 17175 |
Number of constraints which are nor clauses,nor cardinality constraints | 7188 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1115 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc25 THE 2005-05-28 12:58:38 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=24659 boxname=wulflinc25 idbench=1131 idsolver=17 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e465af1c9ec9e748a7782ddbee36d3b1 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos4.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos4.opb IDLAUNCH: 24659 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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: 723692 kB Buffers: 34888 kB Cached: 254896 kB SwapCached: 984 kB Active: 36620 kB Inactive: 255264 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 723440 kB SwapTotal: 2097892 kB SwapFree: 2095996 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5060 kB Slab: 13296 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-28 13:05:04 (client local time) WITH STATUS 1 IN 386.232 SECONDS stats: 24659 7 386.232 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): 1.09 0.99 0.92 2/54 9306 Raw data (stat): 9306 (runsolver) R 9305 1586 1585 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 865000063 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0001 s] Raw data (loadavg): 1.07 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 2044 0 0 0 992 7 0 0 25 0 1 0 865000063 7684096 1371 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 1876 1371 300 300 0 1576 0 vsize: 7504 [startup+20.0006 s] Raw data (loadavg): 1.06 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 2613 0 0 0 1990 9 0 0 25 0 1 0 865000063 9170944 1931 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 2239 1931 300 300 0 1939 0 vsize: 8956 [startup+30.0003 s] Raw data (loadavg): 1.05 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 3833 0 0 0 2988 11 0 0 25 0 1 0 865000063 13410304 2439 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3274 2439 300 300 0 2974 0 vsize: 13096 [startup+40.0013 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 4045 0 0 0 3987 12 0 0 25 0 1 0 865000063 13815808 2646 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3373 2646 300 300 0 3073 0 vsize: 13492 [startup+50.0016 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 4303 0 0 0 4986 13 0 0 25 0 1 0 865000063 14491648 2900 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3538 2900 300 300 0 3238 0 vsize: 14152 [startup+60.0013 s] Raw data (loadavg): 1.03 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 4537 0 0 0 5985 14 0 0 25 0 1 0 865000063 15167488 3130 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3703 3130 300 300 0 3403 0 vsize: 14812 [startup+70.0056 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 4753 0 0 0 6985 15 0 0 25 0 1 0 865000063 15708160 3342 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 3835 3342 300 300 0 3535 0 vsize: 15340 [startup+80.0106 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 9306 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 4952 0 0 0 7985 16 0 0 25 0 1 0 865000063 16248832 3538 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 3967 3538 300 300 0 3667 0 vsize: 15868 [startup+90.1089 s] Raw data (loadavg): 1.10 1.00 0.92 3/57 9341 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 5140 0 0 0 8994 17 0 0 25 0 1 0 865000063 16789504 3723 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 4099 3723 300 300 0 3799 0 vsize: 16396 [startup+100.11 s] Raw data (loadavg): 1.08 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 5317 0 0 0 9986 24 0 0 25 0 1 0 865000063 17195008 3897 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 4198 3897 300 300 0 3898 0 vsize: 16792 [startup+110.109 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 5484 0 0 0 10985 24 0 0 25 0 1 0 865000063 17600512 4062 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 4297 4062 300 300 0 3997 0 vsize: 17188 [startup+120.11 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7487 0 0 0 11982 28 0 0 25 0 1 0 865000063 25403392 4652 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6202 4652 300 300 0 5902 0 vsize: 24808 [startup+130.11 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7541 0 0 0 12982 29 0 0 25 0 1 0 865000063 25403392 4704 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6202 4704 300 300 0 5902 0 vsize: 24808 [startup+140.111 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7594 0 0 0 13981 29 0 0 25 0 1 0 865000063 25403392 4754 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6202 4754 300 300 0 5902 0 vsize: 24808 [startup+150.111 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 9359 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7671 0 0 0 14982 29 0 0 25 0 1 0 865000063 25403392 4829 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6202 4829 300 300 0 5902 0 vsize: 24808 [startup+160.111 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7721 0 0 0 15981 30 0 0 25 0 1 0 865000063 25403392 4877 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6202 4877 300 300 0 5902 0 vsize: 24808 [startup+170.111 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7831 0 0 0 16981 30 0 0 25 0 1 0 865000063 25673728 4985 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6268 4985 300 300 0 5968 0 vsize: 25072 [startup+180.112 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 7963 0 0 0 17981 31 0 0 25 0 1 0 865000063 26079232 5114 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6367 5114 300 300 0 6067 0 vsize: 25468 [startup+190.113 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8090 0 0 0 18980 31 0 0 25 0 1 0 865000063 26349568 5239 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6433 5239 300 300 0 6133 0 vsize: 25732 [startup+200.113 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8214 0 0 0 19980 31 0 0 25 0 1 0 865000063 26755072 5361 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6532 5361 300 300 0 6232 0 vsize: 26128 [startup+210.113 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8336 0 0 0 20980 32 0 0 25 0 1 0 865000063 27025408 5481 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 0 0 0 Raw data (statm): 6598 5481 300 300 0 6298 0 vsize: 26392 [startup+220.113 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8455 0 0 0 21979 32 0 0 25 0 1 0 865000063 27430912 5599 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6697 5599 300 300 0 6397 0 vsize: 26788 [startup+230.113 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8571 0 0 0 22978 33 0 0 25 0 1 0 865000063 27701248 5713 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6763 5713 300 300 0 6463 0 vsize: 27052 [startup+240.113 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8688 0 0 0 23978 34 0 0 25 0 1 0 865000063 27971584 5828 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6829 5828 300 300 0 6529 0 vsize: 27316 [startup+250.113 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8800 0 0 0 24977 34 0 0 25 0 1 0 865000063 28241920 5938 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6895 5938 300 300 0 6595 0 vsize: 27580 [startup+260.113 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 8911 0 0 0 25976 35 0 0 25 0 1 0 865000063 28647424 6047 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 6994 6047 300 300 0 6694 0 vsize: 27976 [startup+270.113 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 9020 0 0 0 26976 35 0 0 25 0 1 0 865000063 28917760 6154 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7060 6154 300 300 0 6760 0 vsize: 28240 [startup+280.113 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 9950 0 0 0 27973 38 0 0 25 0 1 0 865000063 32567296 7083 4294967295 134512640 135726644 3221224576 3221221584 134556171 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 7951 7083 300 300 0 7651 0 vsize: 31804 [startup+290.114 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 46095 0 0 0 28897 114 0 0 25 0 1 0 865000063 151908352 33058 4294967295 134512640 135726644 3221224576 3180962224 134554641 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 37087 33058 300 300 0 36787 0 vsize: 148348 [startup+300.114 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 84428 0 0 0 29822 189 0 0 25 0 1 0 865000063 278597632 52758 4294967295 134512640 135726644 3221224576 3180953228 135105702 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 68017 52758 300 300 0 67717 0 vsize: 272068 [startup+310.133 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 99958 0 0 0 30792 222 0 0 25 0 1 0 865000063 306298880 68023 4294967295 134512640 135726644 3221224576 3180956064 134767076 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 74780 68023 300 300 0 74480 0 vsize: 299120 [startup+320.134 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 130134 0 0 0 31726 288 0 0 25 0 1 0 865000063 418598912 85683 4294967295 134512640 135726644 3221224576 3180955836 134719276 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 102197 85683 300 300 0 101897 0 vsize: 408788 [startup+330.133 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 166354 0 0 0 32658 355 0 0 25 0 1 0 865000063 531816448 102090 4294967295 134512640 135726644 3221224576 3180959292 134604449 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 129838 102090 300 300 0 129538 0 vsize: 519352 [startup+340.135 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 181751 0 0 0 33630 383 0 0 25 0 1 0 865000063 540602368 117219 4294967295 134512640 135726644 3221224576 3180959656 135282351 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 131983 117219 300 300 0 131683 0 vsize: 527932 [startup+350.135 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 224007 0 0 0 34546 468 0 0 25 0 1 0 865000063 668164096 134671 4294967295 134512640 135726644 3221224576 3180956480 134783176 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 163126 134671 300 300 0 162826 0 vsize: 652504 [startup+360.134 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 241302 0 0 0 35514 500 0 0 25 0 1 0 865000063 731643904 151746 4294967295 134512640 135726644 3221224576 3180963292 134604449 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 178624 151746 300 300 0 178324 0 vsize: 714496 [startup+370.134 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 254897 0 0 0 36487 527 0 0 25 0 1 0 865000063 753532928 165169 4294967295 134512640 135726644 3221224576 3184569536 135104009 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 183968 165169 300 300 0 183668 0 vsize: 735872 [startup+380.135 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 254899 0 0 0 37474 540 0 0 25 0 1 0 865000063 441040896 106384 4294967295 134512640 135726644 3221224576 3221222764 135277617 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 107676 106384 300 300 0 107376 0 vsize: 430704 [startup+386.221 s] Raw data (loadavg): 1.00 1.00 0.92 1/53 9361 Raw data (stat): 9306 (pb2sat) R 9305 1586 1585 0 -1 0 254899 0 0 0 37474 540 0 0 25 0 1 0 865000063 441040896 106384 4294967295 134512640 135726644 3221224576 3221222764 135277617 0 0 7 16384 0 0 0 17 1 0 0 Raw data (statm): 107676 106384 300 300 0 107376 0 vsize: 0 Child status: 1 Real time (s): 386.22 CPU time (s): 386.232 CPU user time (s): 380.606 CPU system time (s): 5.62614 CPU usage (%): 100.003 Max. virtual memory (Kb): 735872 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####