Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-arki001.opb |
MD5SUM | d4d0a3fcbcc55e034e04fbd821250726 |
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 | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 2386602666496000 |
Number of bits of the biggest number in a constraint | 52 |
Biggest sum of numbers in a constraint | 5223634990318712 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 81.5566 |
Number of variables | 8268 |
Total number of constraints | 2018 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 436 |
Number of constraints which are nor clauses,nor cardinality constraints | 1582 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 8249 |
LAUNCH ON wulflinc25 THE 2005-09-23 16:45:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8820 boxname=wulflinc25 idbench=616 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d4d0a3fcbcc55e034e04fbd821250726 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-arki001.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-arki001.opb IDLAUNCH: 8820 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.002 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.002 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: 922864 kB Buffers: 17352 kB Cached: 74856 kB SwapCached: 0 kB Active: 47888 kB Inactive: 47240 kB HighTotal: 131008 kB HighFree: 52220 kB LowTotal: 903652 kB LowFree: 870644 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6984 kB Slab: 11128 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 16:47:01 (client local time) WITH STATUS 1 IN 105.895 SECONDS stats: 8820 7 105.895 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/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21694602 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 373 2 364 364 0 9 0 [pid=8355] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-arki001.opb [startup+10.0024 s] Raw data (loadavg): 0.96 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 27902 0 0 0 931 66 0 0 25 0 1 0 21694602 82911232 16745 4294967295 134512640 135987407 3221224560 3221213852 134866211 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 20242 16745 364 364 0 19878 0 [pid=8355] vsize: 80968 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 80968 [startup+20.003 s] Raw data (loadavg): 0.97 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 57954 0 0 0 1868 126 0 0 25 0 1 0 21694602 176234496 35569 4294967295 134512640 135987407 3221224560 3221128888 134930929 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 43026 35569 364 364 0 42662 0 [pid=8355] vsize: 172104 Current children cumulated CPU time (s) 19.94 Current children cumulated vsize (Kb) 172104 [startup+30.0026 s] Raw data (loadavg): 0.97 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 100254 0 0 0 2784 208 0 0 25 0 1 0 21694602 308854784 55668 4294967295 134512640 135987407 3221224560 3221126608 134537491 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 75404 55668 364 364 0 75040 0 [pid=8355] vsize: 301616 Current children cumulated CPU time (s) 29.92 Current children cumulated vsize (Kb) 301616 [startup+40.0032 s] Raw data (loadavg): 0.98 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 117477 0 0 0 3750 240 0 0 25 0 1 0 21694602 366964736 72670 4294967295 134512640 135987407 3221224560 3221130492 135481007 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 89591 72670 364 364 0 89227 0 [pid=8355] vsize: 358364 Current children cumulated CPU time (s) 39.9 Current children cumulated vsize (Kb) 358364 [startup+50.0038 s] Raw data (loadavg): 0.98 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 159471 0 0 0 4664 321 0 0 25 0 1 0 21694602 575365120 113553 4294967295 134512640 135987407 3221224560 3221126428 135500012 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 140470 113553 364 364 0 140106 0 [pid=8355] vsize: 561880 Current children cumulated CPU time (s) 49.85 Current children cumulated vsize (Kb) 561880 [startup+60.0044 s] Raw data (loadavg): 0.98 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 201224 0 0 0 5569 414 0 0 25 0 1 0 21694602 631070720 111783 4294967295 134512640 135987407 3221224560 3221130108 135500006 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 154070 111783 364 364 0 153706 0 [pid=8355] vsize: 616280 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 616280 [startup+70.005 s] Raw data (loadavg): 0.98 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 216477 0 0 0 6536 446 0 0 25 0 1 0 21694602 685711360 126840 4294967295 134512640 135987407 3221224560 3221127872 134861870 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 167410 126840 364 364 0 167046 0 [pid=8355] vsize: 669640 Current children cumulated CPU time (s) 69.82 Current children cumulated vsize (Kb) 669640 [startup+80.0046 s] Raw data (loadavg): 0.99 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 234282 0 0 0 7497 482 0 0 25 0 1 0 21694602 710193152 144418 4294967295 134512640 135987407 3221224560 3221127120 134866122 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 173387 144418 364 364 0 173023 0 [pid=8355] vsize: 693548 Current children cumulated CPU time (s) 79.79 Current children cumulated vsize (Kb) 693548 [startup+90.0052 s] Raw data (loadavg): 0.99 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 252053 0 0 0 8463 515 0 0 25 0 1 0 21694602 735346688 161921 4294967295 134512640 135987407 3221224560 3221127520 134878078 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 179528 161921 364 364 0 179164 0 [pid=8355] vsize: 718112 Current children cumulated CPU time (s) 89.78 Current children cumulated vsize (Kb) 718112 [startup+100.005 s] Raw data (loadavg): 0.99 1.00 0.96 2/55 8355 Raw data (/proc/8355/stat): 8355 (pb2sat) R 8354 8355 4004 0 -1 0 268613 0 0 0 9428 548 0 0 25 0 1 0 21694602 761577472 177911 4294967295 134512640 135987407 3221224560 3221222960 134636917 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8355/statm): 185932 177911 364 364 0 185568 0 [pid=8355] vsize: 743728 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 743728 One traced child (pid=8355) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 106.139 CPU time (s): 105.895 CPU user time (s): 100.045 CPU system time (s): 5.85011 CPU usage (%): 99.7697 Max. virtual memory (cumulated for all children) (Kb): 743728
ERROR: no interpretation found !