Name | mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-bell3b.opb |
MD5SUM | efb36546b6b37df68ff339bb766886b9 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4510472947583472 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1780 |
Biggest coefficient in the objective function | 50331648000000000 |
Number of bits for the biggest coefficient in the objective function | 56 |
Sum of the numbers in the objective function | 1076758128151185266 |
Number of bits of the sum of numbers in the objective function | 60 |
Biggest number in a constraint | 50331648000000000 |
Number of bits of the biggest number in a constraint | 56 |
Biggest sum of numbers in a constraint | 1076758128151185266 |
Number of bits of the biggest sum of numbers | 60 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.08 |
Number of variables | 2283 |
Total number of constraints | 194 |
Number of constraints which are clauses | 22 |
Number of constraints which are cardinality constraints (but not clauses) | 39 |
Number of constraints which are nor clauses,nor cardinality constraints | 133 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 195 |
LAUNCH ON wulflinc29 THE 2005-09-23 16:16:16 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8705 boxname=wulflinc29 idbench=501 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: efb36546b6b37df68ff339bb766886b9 /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-bell3b.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-bell3b.opb IDLAUNCH: 8705 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 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: 925320 kB Buffers: 11680 kB Cached: 80800 kB SwapCached: 0 kB Active: 44268 kB Inactive: 51092 kB HighTotal: 131008 kB HighFree: 50596 kB LowTotal: 903652 kB LowFree: 874724 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6976 kB Slab: 8488 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 16:18:41 (client local time) WITH STATUS 1 IN 145.008 SECONDS stats: 8705 7 145.008 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 59972996232503928 c big objective detected c trying from 0 to 511 c CONFLICT during preprocess c trying from 512 to 1023 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/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 18 0 0 0 0 0 0 0 24 0 1 0 21517403 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 373 2 364 364 0 9 0 [pid=8658] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-bell3b.opb [startup+10.0019 s] Raw data (loadavg): 1.05 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 28152 0 0 0 932 65 0 0 25 0 1 0 21517403 83607552 16990 4294967295 134512640 135987407 3221224560 3221210276 135479922 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 20412 16990 364 364 0 20048 0 [pid=8658] vsize: 81648 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 81648 [startup+20.0027 s] Raw data (loadavg): 1.04 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 54818 0 0 0 1876 121 0 0 25 0 1 0 21517403 160780288 32414 4294967295 134512640 135987407 3221224560 3221207408 134876572 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 39253 32414 364 364 0 38889 0 [pid=8658] vsize: 157012 Current children cumulated CPU time (s) 19.97 Current children cumulated vsize (Kb) 157012 [startup+30.0035 s] Raw data (loadavg): 1.03 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 93962 0 0 0 2791 203 0 0 25 0 1 0 21517403 276164608 49333 4294967295 134512640 135987407 3221224560 3221206768 134856461 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 67423 49333 364 364 0 67059 0 [pid=8658] vsize: 269692 Current children cumulated CPU time (s) 29.94 Current children cumulated vsize (Kb) 269692 [startup+40.0032 s] Raw data (loadavg): 1.03 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 108336 0 0 0 3762 232 0 0 25 0 1 0 21517403 316612608 63456 4294967295 134512640 135987407 3221224560 3221204876 134636944 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 77298 63456 364 364 0 76934 0 [pid=8658] vsize: 309192 Current children cumulated CPU time (s) 39.94 Current children cumulated vsize (Kb) 309192 [startup+50.004 s] Raw data (loadavg): 1.02 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 149410 0 0 0 4675 315 0 0 25 0 1 0 21517403 443879424 84894 4294967295 134512640 135987407 3221224560 3221202908 134636940 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 108369 84894 364 364 0 108005 0 [pid=8658] vsize: 433476 Current children cumulated CPU time (s) 49.9 Current children cumulated vsize (Kb) 433476 [startup+60.0048 s] Raw data (loadavg): 1.02 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 159701 0 0 0 5643 340 0 0 25 0 1 0 21517403 466530304 92844 4294967295 134512640 135987407 3221224560 3221223248 134811870 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 113899 92844 364 364 0 113535 0 [pid=8658] vsize: 455596 Current children cumulated CPU time (s) 59.83 Current children cumulated vsize (Kb) 455596 [startup+70.0056 s] Raw data (loadavg): 1.02 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 160405 0 0 0 6624 348 0 0 25 0 1 0 21517403 469852160 93548 4294967295 134512640 135987407 3221224560 3221223248 134811816 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 114710 93548 364 364 0 114346 0 [pid=8658] vsize: 458840 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 458840 [startup+80.0064 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 161069 0 0 0 7613 353 0 0 25 0 1 0 21517403 473161728 94212 4294967295 134512640 135987407 3221224560 3221223248 134811729 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8658/statm): 115518 94212 364 364 0 115154 0 [pid=8658] vsize: 462072 Current children cumulated CPU time (s) 79.66 Current children cumulated vsize (Kb) 462072 [startup+90.0062 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 189868 0 0 0 8543 415 0 0 25 0 1 0 21517403 677203968 122934 4294967295 134512640 135987407 3221224560 3220813712 134887647 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 165333 122934 364 364 0 164969 0 [pid=8658] vsize: 661332 Current children cumulated CPU time (s) 89.58 Current children cumulated vsize (Kb) 661332 [startup+100.007 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 208021 0 0 0 9494 461 0 0 25 0 1 0 21517403 637710336 116267 4294967295 134512640 135987407 3221224560 3220884368 134877726 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 155691 116267 364 364 0 155327 0 [pid=8658] vsize: 622764 Current children cumulated CPU time (s) 99.55 Current children cumulated vsize (Kb) 622764 [startup+110.008 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 225879 0 0 0 10452 501 0 0 25 0 1 0 21517403 666652672 133895 4294967295 134512640 135987407 3221224560 3220653692 134637002 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 162757 133895 364 364 0 162393 0 [pid=8658] vsize: 651028 Current children cumulated CPU time (s) 109.53 Current children cumulated vsize (Kb) 651028 [startup+120.009 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 245225 0 0 0 11412 538 0 0 25 0 1 0 21517403 698310656 152994 4294967295 134512640 135987407 3221224560 3221149232 134635423 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8658/statm): 170486 152995 364 364 0 170122 0 [pid=8658] vsize: 681944 Current children cumulated CPU time (s) 119.5 Current children cumulated vsize (Kb) 681944 [startup+130.009 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 260925 0 0 0 12374 575 0 0 25 0 1 0 21517403 737583104 166307 4294967295 134512640 135987407 3221224560 3221222968 134827499 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/8658/statm): 180074 166307 364 364 0 179710 0 [pid=8658] vsize: 720296 Current children cumulated CPU time (s) 129.49 Current children cumulated vsize (Kb) 720296 [startup+140.009 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 8658 Raw data (/proc/8658/stat): 8658 (pb2sat) R 8657 8658 4005 0 -1 0 287969 0 0 0 13298 643 0 0 25 0 1 0 21517403 831733760 189277 4294967295 134512640 135987407 3221224560 3221223376 134802471 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8658/statm): 203060 189277 364 364 0 202696 0 [pid=8658] vsize: 812240 Current children cumulated CPU time (s) 139.41 Current children cumulated vsize (Kb) 812240 One traced child (pid=8658) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 145.601 CPU time (s): 145.008 CPU user time (s): 138.184 CPU system time (s): 6.82396 CPU usage (%): 99.5925 Max. virtual memory (cumulated for all children) (Kb): 812240
ERROR: no interpretation found !