Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-shell.opb |
MD5SUM | 0f9e797b4b986a37159e9b1332a4b629 |
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 | 39844 |
Biggest coefficient in the objective function | 2101312749568 |
Number of bits for the biggest coefficient in the objective function | 41 |
Sum of the numbers in the objective function | 249967315526150 |
Number of bits of the sum of numbers in the objective function | 48 |
Biggest number in a constraint | 2101312749568 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 249967315526150 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.398939 |
Number of variables | 45231 |
Total number of constraints | 653 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 653 |
Minimum length of a constraint | 19 |
Maximum length of a constraint | 1560 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc2 THE 2005-06-09 04:26:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29093 boxname=wulflinc2 idbench=877 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: 0f9e797b4b986a37159e9b1332a4b629 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-shell.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-20-10-shell.opb IDLAUNCH: 29093 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.191 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.191 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: 813052 kB Buffers: 24320 kB Cached: 172216 kB SwapCached: 4472 kB Active: 31036 kB Inactive: 170556 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 812800 kB SwapTotal: 2097136 kB SwapFree: 2091616 kB Dirty: 28 kB Writeback: 0 kB Mapped: 4992 kB Slab: 14316 kB Committed_AS: 71792 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 04:32:29 (client local time) WITH STATUS 20 IN 347.269 SECONDS stats: 29093 7 347.269 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c Initial problem consists of 45231 variables and 973 constraints. s UNSATISFIABLE c Exit Code: 20 c Total time: 347.209 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 Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.71 0.91 0.89 1/54 19864 Raw data (stat): 19864 (runsolver) R 19863 31399 31398 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 907389364 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0007 s] Raw data (loadavg): 0.76 0.91 0.89 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 1053 0 0 0 995 3 0 0 25 0 1 0 907389364 16707584 973 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4079 973 1111 63 0 4016 0 vsize: 16316 [startup+20.0014 s] Raw data (loadavg): 0.79 0.91 0.89 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 1444 0 0 0 1994 4 0 0 25 0 1 0 907389364 18190336 1364 4294967295 134512640 134716908 3221224560 3221222788 1077414385 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4441 1364 1111 63 0 4378 0 vsize: 17764 [startup+30.0016 s] Raw data (loadavg): 0.82 0.92 0.89 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 1845 0 0 0 2993 5 0 0 25 0 1 0 907389364 19832832 1765 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4842 1765 1111 63 0 4779 0 vsize: 19368 [startup+40.0013 s] Raw data (loadavg): 0.85 0.92 0.89 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 2227 0 0 0 3992 6 0 0 25 0 1 0 907389364 21483520 2147 4294967295 134512640 134716908 3221224560 3221222788 1077414357 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5245 2147 1111 63 0 5182 0 vsize: 20980 [startup+50.0025 s] Raw data (loadavg): 0.87 0.92 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 2634 0 0 0 4991 6 0 0 25 0 1 0 907389364 23126016 2554 4294967295 134512640 134716908 3221224560 3221222788 1077414336 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5646 2554 1111 63 0 5583 0 vsize: 22584 [startup+60.0027 s] Raw data (loadavg): 0.89 0.92 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 3084 0 0 0 5990 8 0 0 25 0 1 0 907389364 25038848 3004 4294967295 134512640 134716908 3221224560 3221222788 1077414360 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6113 3004 1111 63 0 6050 0 vsize: 24452 [startup+70.0024 s] Raw data (loadavg): 0.91 0.92 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 3489 0 0 0 6989 9 0 0 25 0 1 0 907389364 26693632 3409 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6517 3409 1111 63 0 6454 0 vsize: 26068 [startup+80.0036 s] Raw data (loadavg): 0.92 0.93 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 3901 0 0 0 7989 10 0 0 25 0 1 0 907389364 28344320 3821 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6920 3821 1111 63 0 6857 0 vsize: 27680 [startup+90.0038 s] Raw data (loadavg): 0.93 0.93 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 4321 0 0 0 8988 11 0 0 25 0 1 0 907389364 29999104 4241 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7324 4241 1111 63 0 7261 0 vsize: 29296 [startup+100.005 s] Raw data (loadavg): 0.94 0.93 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 4771 0 0 0 9987 12 0 0 25 0 1 0 907389364 31956992 4691 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7802 4691 1111 63 0 7739 0 vsize: 31208 [startup+110.006 s] Raw data (loadavg): 0.95 0.93 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 5233 0 0 0 10986 12 0 0 25 0 1 0 907389364 33751040 5153 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8240 5153 1111 63 0 8177 0 vsize: 32960 [startup+120.006 s] Raw data (loadavg): 0.96 0.93 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 5689 0 0 0 11985 13 0 0 25 0 1 0 907389364 35700736 5609 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8716 5609 1111 63 0 8653 0 vsize: 34864 [startup+130.006 s] Raw data (loadavg): 0.96 0.94 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 6152 0 0 0 12984 15 0 0 25 0 1 0 907389364 37502976 6072 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9156 6072 1111 63 0 9093 0 vsize: 36624 [startup+140.006 s] Raw data (loadavg): 0.97 0.94 0.90 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 6631 0 0 0 13984 16 0 0 25 0 1 0 907389364 39456768 6551 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9633 6551 1111 63 0 9570 0 vsize: 38532 [startup+150.007 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 7124 0 0 0 14983 17 0 0 25 0 1 0 907389364 41558016 7044 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10146 7044 1111 63 0 10083 0 vsize: 40584 [startup+160.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 7626 0 0 0 15982 17 0 0 25 0 1 0 907389364 43634688 7546 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10653 7546 1111 63 0 10590 0 vsize: 42612 [startup+170.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 8140 0 0 0 16981 19 0 0 25 0 1 0 907389364 45731840 8060 4294967295 134512640 134716908 3221224560 3221222788 1077414376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11165 8060 1111 63 0 11102 0 vsize: 44660 [startup+180.007 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 8687 0 0 0 17979 21 0 0 25 0 1 0 907389364 48058368 8607 4294967295 134512640 134716908 3221224560 3221222788 1077414351 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11733 8607 1111 63 0 11670 0 vsize: 46932 [startup+190.008 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 9238 0 0 0 18977 23 0 0 25 0 1 0 907389364 50278400 9158 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12275 9158 1111 63 0 12212 0 vsize: 49100 [startup+200.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 9817 0 0 0 19976 25 0 0 25 0 1 0 907389364 52678656 9737 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12861 9737 1111 63 0 12798 0 vsize: 51444 [startup+210.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 10421 0 0 0 20975 26 0 0 25 0 1 0 907389364 55050240 10341 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 13440 10341 1111 63 0 13377 0 vsize: 53760 [startup+220.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 11048 0 0 0 21973 27 0 0 25 0 1 0 907389364 57606144 10968 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 14064 10968 1111 63 0 14001 0 vsize: 56256 [startup+230.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 11715 0 0 0 22972 29 0 0 25 0 1 0 907389364 60440576 11635 4294967295 134512640 134716908 3221224560 3221223216 134527930 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 14756 11635 1111 63 0 14693 0 vsize: 59024 [startup+240.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 12393 0 0 0 23971 30 0 0 25 0 1 0 907389364 63119360 12313 4294967295 134512640 134716908 3221224560 3221222788 1077414370 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 15410 12313 1111 63 0 15347 0 vsize: 61640 [startup+250.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 13097 0 0 0 24969 32 0 0 25 0 1 0 907389364 65966080 13017 4294967295 134512640 134716908 3221224560 3221222788 1077414374 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 16105 13017 1111 63 0 16042 0 vsize: 64420 [startup+260.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 13817 0 0 0 25968 34 0 0 25 0 1 0 907389364 68956160 13737 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 16835 13737 1111 63 0 16772 0 vsize: 67340 [startup+270.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 14561 0 0 0 26967 35 0 0 25 0 1 0 907389364 71929856 14481 4294967295 134512640 134716908 3221224560 3221223216 134527930 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 17561 14481 1111 63 0 17498 0 vsize: 70244 [startup+280.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 15348 0 0 0 27965 37 0 0 25 0 1 0 907389364 75235328 15268 4294967295 134512640 134716908 3221224560 3221223216 134527946 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 18368 15268 1111 63 0 18305 0 vsize: 73472 [startup+290.009 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 16183 0 0 0 28963 39 0 0 25 0 1 0 907389364 78651392 16103 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 19202 16103 1111 63 0 19139 0 vsize: 76808 [startup+300.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 17068 0 0 0 29961 41 0 0 25 0 1 0 907389364 82419712 16988 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20122 16988 1111 63 0 20059 0 vsize: 80488 [startup+310.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 17938 0 0 0 30960 42 0 0 25 0 1 0 907389364 85999616 17858 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 20996 17858 1111 63 0 20933 0 vsize: 83984 [startup+320.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 18849 0 0 0 31957 45 0 0 25 0 1 0 907389364 89755648 18769 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 21913 18769 1111 63 0 21850 0 vsize: 87652 [startup+330.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 19790 0 0 0 32956 46 0 0 25 0 1 0 907389364 93626368 19710 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 22858 19710 1111 63 0 22795 0 vsize: 91432 [startup+340.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 23070 0 0 0 33948 54 0 0 25 0 1 0 907389364 106323968 22830 4294967295 134512640 134716908 3221224560 3221223204 1077374550 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25958 22830 1111 63 0 25895 0 vsize: 103832 [startup+347.245 s] Raw data (loadavg): 0.99 0.96 0.91 1/53 19864 Raw data (stat): 19864 (bsolo_lpr_cuts-) R 19863 31399 31398 0 -1 0 23070 0 0 0 33948 54 0 0 25 0 1 0 907389364 106323968 22830 4294967295 134512640 134716908 3221224560 3221223204 1077374550 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 25958 22830 1111 63 0 25895 0 vsize: 0 Child status: 20 Real time (s): 347.245 CPU time (s): 347.269 CPU user time (s): 346.527 CPU system time (s): 0.741887 CPU usage (%): 100.007 Max. virtual memory (Kb): 103832 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####