Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp98ar.opb |
MD5SUM | 9565d6b3010c78b37c39352cc9731cb7 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 7346652384 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 15085 |
Biggest coefficient in the objective function | 504328818 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 2067304124713 |
Number of bits of the sum of numbers in the objective function | 41 |
Biggest number in a constraint | 504328818 |
Number of bits of the biggest number in a constraint | 29 |
Biggest sum of numbers in a constraint | 2067304124713 |
Number of bits of the biggest sum of numbers | 41 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1207.19 |
Number of variables | 15085 |
Total number of constraints | 16520 |
Number of constraints which are clauses | 181 |
Number of constraints which are cardinality constraints (but not clauses) | 15927 |
Number of constraints which are nor clauses,nor cardinality constraints | 412 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 4222 |
LAUNCH ON wulflinc32 THE 2005-09-23 19:15:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9361 boxname=wulflinc32 idbench=1157 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 9565d6b3010c78b37c39352cc9731cb7 /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-sp98ar.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-sp98ar.opb IDLAUNCH: 9361 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.145 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.145 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: 1034724 kB MemFree: 899988 kB Buffers: 16012 kB Cached: 98568 kB SwapCached: 0 kB Active: 49380 kB Inactive: 68072 kB HighTotal: 131072 kB HighFree: 31168 kB LowTotal: 903652 kB LowFree: 868820 kB SwapTotal: 2097892 kB SwapFree: 2097892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6988 kB Slab: 11584 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-23 19:17:37 (client local time) WITH STATUS 1 IN 147.539 SECONDS stats: 9361 7 147.539 1
c This solver internally uses Chaff 2004.11.15 Simplified c running zchaff... c got solution with objective value: 40382066383 c big objective detected c trying from 0 to 511 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/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22588380 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 373 2 364 364 0 9 0 [pid=10275] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc32/normalized-mps-v2-13-7-sp98ar.opb [startup+10.0018 s] Raw data (loadavg): 0.94 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 13087 0 0 0 963 33 0 0 25 0 1 0 22588380 40058880 7534 4294967295 134512640 135987407 3221224560 3220910144 134862189 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 9780 7534 364 364 0 9416 0 [pid=10275] vsize: 39120 Current children cumulated CPU time (s) 9.96 Current children cumulated vsize (Kb) 39120 [startup+20.0026 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 39390 0 0 0 1903 90 0 0 25 0 1 0 22588380 118841344 23279 4294967295 134512640 135987407 3221224560 3219819200 134640555 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 29014 23279 364 364 0 28650 0 [pid=10275] vsize: 116056 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 116056 [startup+30.0024 s] Raw data (loadavg): 0.95 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 57932 0 0 0 2858 134 0 0 25 0 1 0 22588380 165515264 35462 4294967295 134512640 135987407 3221224560 3221221952 134616295 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 40409 35462 364 364 0 40045 0 [pid=10275] vsize: 161636 Current children cumulated CPU time (s) 29.92 Current children cumulated vsize (Kb) 161636 [startup+40.0031 s] Raw data (loadavg): 0.96 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 96281 0 0 0 3776 215 0 0 25 0 1 0 22588380 282251264 51615 4294967295 134512640 135987407 3221224560 3220845308 134677714 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 68909 51615 364 364 0 68545 0 [pid=10275] vsize: 275636 Current children cumulated CPU time (s) 39.91 Current children cumulated vsize (Kb) 275636 [startup+50.0039 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 105425 0 0 0 4747 242 0 0 25 0 1 0 22588380 318914560 60594 4294967295 134512640 135987407 3221224560 3220792432 134854925 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 77860 60594 364 364 0 77496 0 [pid=10275] vsize: 311440 Current children cumulated CPU time (s) 49.89 Current children cumulated vsize (Kb) 311440 [startup+60.0037 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 115077 0 0 0 5722 267 0 0 25 0 1 0 22588380 322834432 70076 4294967295 134512640 135987407 3221224560 3220802416 134887785 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 78817 70076 364 364 0 78453 0 [pid=10275] vsize: 315268 Current children cumulated CPU time (s) 59.89 Current children cumulated vsize (Kb) 315268 [startup+70.0045 s] Raw data (loadavg): 0.97 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 153680 0 0 0 6641 342 0 0 25 0 1 0 22588380 449695744 89093 4294967295 134512640 135987407 3221224560 3220517580 135499883 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 109789 89093 364 364 0 109425 0 [pid=10275] vsize: 439156 Current children cumulated CPU time (s) 69.83 Current children cumulated vsize (Kb) 439156 [startup+80.0052 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 188205 0 0 0 7564 419 0 0 25 0 1 0 22588380 562688000 96477 4294967295 134512640 135987407 3221224560 3221223248 134812053 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 137375 96477 364 364 0 137011 0 [pid=10275] vsize: 549500 Current children cumulated CPU time (s) 79.83 Current children cumulated vsize (Kb) 549500 [startup+90.006 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 192277 0 0 0 8542 433 0 0 25 0 1 0 22588380 579596288 100122 4294967295 134512640 135987407 3221224560 3221223248 134811805 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10275/statm): 141503 100122 364 364 0 141139 0 [pid=10275] vsize: 566012 Current children cumulated CPU time (s) 89.75 Current children cumulated vsize (Kb) 566012 [startup+100.006 s] Raw data (loadavg): 0.98 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 192277 0 0 0 9528 437 0 0 25 0 1 0 22588380 579596288 100122 4294967295 134512640 135987407 3221224560 3221223120 134788496 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10275/statm): 141503 100122 364 364 0 141139 0 [pid=10275] vsize: 566012 Current children cumulated CPU time (s) 99.65 Current children cumulated vsize (Kb) 566012 [startup+110.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 192332 0 0 0 10514 442 0 0 25 0 1 0 22588380 579768320 100176 4294967295 134512640 135987407 3221224560 3220978496 134856505 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10275/statm): 141545 100176 364 364 0 141181 0 [pid=10275] vsize: 566180 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 566180 [startup+120.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 210190 0 0 0 11469 486 0 0 25 0 1 0 22588380 640503808 117793 4294967295 134512640 135987407 3221224560 3219238828 135482121 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10275/statm): 156373 117793 364 364 0 156009 0 [pid=10275] vsize: 625492 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 625492 [startup+130.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 230882 0 0 0 12418 533 0 0 25 0 1 0 22588380 674566144 138224 4294967295 134512640 135987407 3221224560 3220571408 134537491 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10275/statm): 164689 138225 364 364 0 164325 0 [pid=10275] vsize: 658756 Current children cumulated CPU time (s) 129.51 Current children cumulated vsize (Kb) 658756 [startup+140.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/55 10275 Raw data (/proc/10275/stat): 10275 (pb2sat) R 10274 10275 4005 0 -1 0 250944 0 0 0 13370 578 0 0 25 0 1 0 22588380 707682304 158028 4294967295 134512640 135987407 3221224560 3217900928 134887887 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/10275/statm): 172774 158030 364 364 0 172410 0 [pid=10275] vsize: 691096 Current children cumulated CPU time (s) 139.48 Current children cumulated vsize (Kb) 691096 One traced child (pid=10275) exited with status: 1 All traced children have exited ! Game is over. Child status: 1 Real time (s): 148.057 CPU time (s): 147.539 CPU user time (s): 141.266 CPU system time (s): 6.27305 CPU usage (%): 99.6496 Max. virtual memory (cumulated for all children) (Kb): 691096
ERROR: no interpretation found !