Name | mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-rd-rplusc-21.opb |
MD5SUM | 62166f7982a2b3c488537a2a2dbe4149 |
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 | 35 |
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 | 3735451 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 383602153706972160 |
Number of bits of the biggest number in a constraint | 59 |
Biggest sum of numbers in a constraint | 772928706545624815 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 290.495 |
Number of variables | 2644 |
Total number of constraints | 126450 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 699 |
Number of constraints which are nor clauses,nor cardinality constraints | 125751 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 130 |
LAUNCH ON wulflinc21 THE 2005-09-23 18:17:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9183 boxname=wulflinc21 idbench=979 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 62166f7982a2b3c488537a2a2dbe4149 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb IDLAUNCH: 9183 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.188 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.188 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: 748320 kB Buffers: 14452 kB Cached: 252992 kB SwapCached: 0 kB Active: 209820 kB Inactive: 60552 kB HighTotal: 131008 kB HighFree: 3724 kB LowTotal: 903652 kB LowFree: 744596 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 0 kB Writeback: 0 kB Mapped: 6984 kB Slab: 10180 kB Committed_AS: 63632 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 18:19:58 (client local time) WITH STATUS 1 IN 148.635 SECONDS stats: 9183 7 148.635 1
c This solver internally uses Chaff 2004.11.15 Simplified Unexpected exception : St9bad_alloc
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22281886 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 373 2 364 364 0 9 0 [pid=10896] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-rd-rplusc-21.opb [startup+10.0029 s] Raw data (loadavg): 1.07 1.03 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 1593 0 0 0 990 7 0 0 25 0 1 0 22281886 6017024 966 4294967295 134512640 135987407 3221224560 3221221820 134669194 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 1469 966 364 364 0 1105 0 [pid=10896] vsize: 5876 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 5876 [startup+20.0036 s] Raw data (loadavg): 1.06 1.03 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 2988 0 0 0 1978 16 0 0 25 0 1 0 22281886 10039296 1676 4294967295 134512640 135987407 3221224560 3221221952 134616236 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 2451 1676 364 364 0 2087 0 [pid=10896] vsize: 9804 Current children cumulated CPU time (s) 19.94 Current children cumulated vsize (Kb) 9804 [startup+30.0043 s] Raw data (loadavg): 1.05 1.03 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 4489 0 0 0 2968 23 0 0 25 0 1 0 22281886 15073280 2556 4294967295 134512640 135987407 3221224560 3221221952 134616278 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 3680 2556 364 364 0 3316 0 [pid=10896] vsize: 14720 Current children cumulated CPU time (s) 29.91 Current children cumulated vsize (Kb) 14720 [startup+40.004 s] Raw data (loadavg): 1.04 1.03 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 5817 0 0 0 3958 30 0 0 25 0 1 0 22281886 18354176 3103 4294967295 134512640 135987407 3221224560 3221221952 134616295 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 4481 3103 364 364 0 4117 0 [pid=10896] vsize: 17924 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 17924 [startup+50.0047 s] Raw data (loadavg): 1.04 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 6396 0 0 0 4950 37 0 0 25 0 1 0 22281886 20586496 3671 4294967295 134512640 135987407 3221224560 3221221952 134616261 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 5026 3671 364 364 0 4662 0 [pid=10896] vsize: 20104 Current children cumulated CPU time (s) 49.87 Current children cumulated vsize (Kb) 20104 [startup+60.0044 s] Raw data (loadavg): 1.03 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 25706 0 0 0 5904 81 0 0 25 0 1 0 22281886 78573568 14591 4294967295 134512640 135987407 3221224560 3221206448 134878315 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 19183 14591 364 364 0 18819 0 [pid=10896] vsize: 76732 Current children cumulated CPU time (s) 59.85 Current children cumulated vsize (Kb) 76732 [startup+70.005 s] Raw data (loadavg): 1.03 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 56410 0 0 0 6837 145 0 0 25 0 1 0 22281886 183693312 33998 4294967295 134512640 135987407 3221224560 3221208920 134537317 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 44847 33998 364 364 0 44483 0 [pid=10896] vsize: 179388 Current children cumulated CPU time (s) 69.82 Current children cumulated vsize (Kb) 179388 [startup+80.0057 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 88802 0 0 0 7772 207 0 0 25 0 1 0 22281886 268898304 55749 4294967295 134512640 135987407 3221224560 3221206332 135484990 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 65649 55749 364 364 0 65285 0 [pid=10896] vsize: 262596 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 262596 [startup+90.0054 s] Raw data (loadavg): 1.02 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 117883 0 0 0 8709 268 0 0 25 0 1 0 22281886 377249792 72314 4294967295 134512640 135987407 3221224560 3221208188 134637002 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 92102 72314 364 364 0 91738 0 [pid=10896] vsize: 368408 Current children cumulated CPU time (s) 89.77 Current children cumulated vsize (Kb) 368408 [startup+100.006 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 162928 0 0 0 9614 358 0 0 25 0 1 0 22281886 517820416 95484 4294967295 134512640 135987407 3221224560 3221206880 134537371 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 126421 95484 364 364 0 126057 0 [pid=10896] vsize: 505684 Current children cumulated CPU time (s) 99.72 Current children cumulated vsize (Kb) 505684 [startup+110.007 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 182316 0 0 0 10577 392 0 0 25 0 1 0 22281886 545935360 114611 4294967295 134512640 135987407 3221224560 3221207096 135487946 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 133285 114611 364 364 0 132921 0 [pid=10896] vsize: 533140 Current children cumulated CPU time (s) 109.69 Current children cumulated vsize (Kb) 533140 [startup+120.007 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 223531 0 0 0 11490 478 0 0 25 0 1 0 22281886 670793728 131024 4294967295 134512640 135987407 3221224560 3221206204 135479970 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 163768 131024 364 364 0 163404 0 [pid=10896] vsize: 655072 Current children cumulated CPU time (s) 119.68 Current children cumulated vsize (Kb) 655072 [startup+130.008 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 239809 0 0 0 12457 509 0 0 25 0 1 0 22281886 728002560 147083 4294967295 134512640 135987407 3221224560 3221206188 135486712 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 177735 147083 364 364 0 177371 0 [pid=10896] vsize: 710940 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 710940 [startup+140.008 s] Raw data (loadavg): 1.01 1.02 0.94 2/55 10896 Raw data (/proc/10896/stat): 10896 (pb2sat) R 10895 10896 4059 0 -1 0 260620 0 0 0 13416 548 0 0 25 0 1 0 22281886 763441152 165982 4294967295 134512640 135987407 3221224560 3221208272 134887887 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10896/statm): 186387 165982 364 364 0 186023 0 [pid=10896] vsize: 745548 Current children cumulated CPU time (s) 139.64 Current children cumulated vsize (Kb) 745548 One traced child (pid=10896) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 149.004 CPU time (s): 148.635 CPU user time (s): 142.748 CPU system time (s): 5.8871 CPU usage (%): 99.7523 Max. virtual memory (cumulated for all children) (Kb): 745548
ERROR: no interpretation found !