Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ar98.opb |
MD5SUM | 53176d06e1e99afe2d28ec1484235311 |
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 | 21 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 2097151 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 81920000000 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 40410384871329 |
Number of bits of the biggest sum of numbers | 46 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 6.22305 |
Number of variables | 18824 |
Total number of constraints | 17064 |
Number of constraints which are clauses | 1 |
Number of constraints which are cardinality constraints (but not clauses) | 16718 |
Number of constraints which are nor clauses,nor cardinality constraints | 345 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 15827 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-04-20 22:28:06 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=19966 boxname=wulflinc21 idbench=1536 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 53176d06e1e99afe2d28ec1484235311 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-blp-ar98.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-blp-ar98.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-blp-ar98.opb IDLAUNCH: 19966 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 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: 251968 kB Buffers: 17900 kB Cached: 740708 kB SwapCached: 0 kB Active: 126660 kB Inactive: 634864 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 251716 kB SwapTotal: 2097892 kB SwapFree: 2097804 kB Dirty: 0 kB Writeback: 0 kB Mapped: 6948 kB Slab: 15460 kB Committed_AS: 63788 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 22:33:14 (client local time) WITH STATUS 1 IN 307.434 SECONDS stats: 19966 7 307.434 1 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... PARSE ERROR! [line 32096] Integer overflow. Big numbers not supported yet. #### 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.10 0.99 0.93 2/55 30158 Raw data (stat): 30158 (runsolver) R 30157 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 417302032 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99949 s] Raw data (loadavg): 1.08 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 582 0 0 0 997 1 0 0 25 0 1 0 417302032 4153344 560 4294967295 134512640 134672761 3221224544 3221223852 1075372046 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1014 560 603 41 0 973 0 vsize: 4056 [startup+20.0001 s] Raw data (loadavg): 1.07 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 750 0 0 0 1997 2 0 0 25 0 1 0 417302032 5345280 728 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1305 728 603 41 0 1264 0 vsize: 5220 [startup+29.9998 s] Raw data (loadavg): 1.06 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 834 0 0 0 2997 2 0 0 25 0 1 0 417302032 5517312 812 4294967295 134512640 134672761 3221224544 3221223836 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1347 812 603 41 0 1306 0 vsize: 5388 [startup+39.9995 s] Raw data (loadavg): 1.05 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 873 0 0 0 3996 3 0 0 25 0 1 0 417302032 5517312 851 4294967295 134512640 134672761 3221224544 3221223852 1075372048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1347 851 603 41 0 1306 0 vsize: 5388 [startup+50.0002 s] Raw data (loadavg): 1.04 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 928 0 0 0 4997 3 0 0 25 0 1 0 417302032 5517312 906 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1347 906 603 41 0 1306 0 vsize: 5388 [startup+60.0079 s] Raw data (loadavg): 1.03 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 973 0 0 0 5997 3 0 0 25 0 1 0 417302032 5648384 951 4294967295 134512640 134672761 3221224544 3221223836 1075372044 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1379 951 603 41 0 1338 0 vsize: 5516 [startup+70.0085 s] Raw data (loadavg): 1.03 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1190 0 0 0 6997 4 0 0 25 0 1 0 417302032 7979008 1168 4294967295 134512640 134672761 3221224544 3221223836 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1948 1168 603 41 0 1907 0 vsize: 7792 [startup+80.0092 s] Raw data (loadavg): 1.02 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1204 0 0 0 7997 4 0 0 25 0 1 0 417302032 7983104 1182 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1949 1182 603 41 0 1908 0 vsize: 7796 [startup+90.0089 s] Raw data (loadavg): 1.02 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1257 0 0 0 8996 5 0 0 25 0 1 0 417302032 8089600 1235 4294967295 134512640 134672761 3221224544 3221223852 1075372068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1975 1235 603 41 0 1934 0 vsize: 7900 [startup+100.009 s] Raw data (loadavg): 1.02 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1296 0 0 0 9995 5 0 0 25 0 1 0 417302032 8351744 1274 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2039 1274 603 41 0 1998 0 vsize: 8156 [startup+110.008 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1327 0 0 0 10995 6 0 0 25 0 1 0 417302032 8441856 1305 4294967295 134512640 134672761 3221224544 3221223852 1075372040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2061 1305 603 41 0 2020 0 vsize: 8244 [startup+120.009 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1382 0 0 0 11995 6 0 0 25 0 1 0 417302032 8769536 1360 4294967295 134512640 134672761 3221224544 3221223872 134586555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2141 1360 603 41 0 2100 0 vsize: 8564 [startup+130.01 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1389 0 0 0 12995 6 0 0 25 0 1 0 417302032 8769536 1367 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2141 1367 603 41 0 2100 0 vsize: 8564 [startup+140.009 s] Raw data (loadavg): 1.01 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1470 0 0 0 13995 7 0 0 25 0 1 0 417302032 8990720 1434 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2195 1434 603 41 0 2154 0 vsize: 8780 [startup+150.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1554 0 0 0 14995 7 0 0 25 0 1 0 417302032 9351168 1508 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2283 1508 603 41 0 2242 0 vsize: 9132 [startup+160.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1589 0 0 0 15994 7 0 0 25 0 1 0 417302032 9465856 1543 4294967295 134512640 134672761 3221224544 3221223852 1075372065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2311 1543 603 41 0 2270 0 vsize: 9244 [startup+170.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1642 0 0 0 16994 8 0 0 25 0 1 0 417302032 9732096 1596 4294967295 134512640 134672761 3221224544 3221223852 1075372048 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2376 1596 603 41 0 2335 0 vsize: 9504 [startup+180.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1694 0 0 0 17993 9 0 0 25 0 1 0 417302032 9965568 1648 4294967295 134512640 134672761 3221224544 3221223852 1075372060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2433 1648 603 41 0 2392 0 vsize: 9732 [startup+190.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1786 0 0 0 18993 10 0 0 25 0 1 0 417302032 10391552 1740 4294967295 134512640 134672761 3221224544 3221223852 134516148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2537 1740 603 41 0 2496 0 vsize: 10148 [startup+200.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1837 0 0 0 19992 10 0 0 25 0 1 0 417302032 10539008 1791 4294967295 134512640 134672761 3221224544 3221223852 1075372040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2573 1791 603 41 0 2532 0 vsize: 10292 [startup+210.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1913 0 0 0 20991 11 0 0 25 0 1 0 417302032 10887168 1867 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2658 1867 603 41 0 2617 0 vsize: 10632 [startup+220.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 1985 0 0 0 21991 11 0 0 25 0 1 0 417302032 11116544 1929 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2714 1929 603 41 0 2673 0 vsize: 10856 [startup+230.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2091 0 0 0 22990 12 0 0 25 0 1 0 417302032 11632640 2026 4294967295 134512640 134672761 3221224544 3221223852 134516148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2840 2026 603 41 0 2799 0 vsize: 11360 [startup+240.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2167 0 0 0 23990 13 0 0 25 0 1 0 417302032 11935744 2102 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2914 2102 603 41 0 2873 0 vsize: 11656 [startup+250.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2239 0 0 0 24989 14 0 0 25 0 1 0 417302032 12304384 2174 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3004 2174 603 41 0 2963 0 vsize: 12016 [startup+260.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2299 0 0 0 25989 14 0 0 25 0 1 0 417302032 12673024 2234 4294967295 134512640 134672761 3221224544 3221223872 134586518 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3094 2234 603 41 0 3053 0 vsize: 12376 [startup+270.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2344 0 0 0 26989 14 0 0 25 0 1 0 417302032 12759040 2279 4294967295 134512640 134672761 3221224544 3221223852 1075372042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3115 2279 603 41 0 3074 0 vsize: 12460 [startup+280.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2417 0 0 0 27989 15 0 0 25 0 1 0 417302032 13115392 2352 4294967295 134512640 134672761 3221224544 3221223852 1075372044 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3202 2352 603 41 0 3161 0 vsize: 12808 [startup+290.01 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2493 0 0 0 28989 15 0 0 25 0 1 0 417302032 13430784 2428 4294967295 134512640 134672761 3221224544 3221223872 134586520 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3279 2428 603 41 0 3238 0 vsize: 13116 [startup+300.011 s] Raw data (loadavg): 1.00 0.99 0.93 2/55 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2557 0 0 0 29989 15 0 0 25 0 1 0 417302032 13778944 2492 4294967295 134512640 134672761 3221224544 3221223852 1075372060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3364 2492 603 41 0 3323 0 vsize: 13456 [startup+307.397 s] Raw data (loadavg): 1.00 0.99 0.93 1/54 30158 Raw data (stat): 30158 (minisat+) R 30157 30927 30926 0 -1 0 2557 0 0 0 29989 15 0 0 25 0 1 0 417302032 13778944 2492 4294967295 134512640 134672761 3221224544 3221223852 1075372060 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3364 2492 603 41 0 3323 0 vsize: 0 Child status: 1 Real time (s): 307.397 CPU time (s): 307.434 CPU user time (s): 307.265 CPU system time (s): 0.168974 CPU usage (%): 100.012 Max. virtual memory (Kb): 13456 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####