Name | mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-sctap2.opb |
MD5SUM | c5a9e8be191d07f712a0a357db2fa392 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 65305313280 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 42300 |
Biggest coefficient in the objective function | 42949672960 |
Number of bits for the biggest coefficient in the objective function | 36 |
Sum of the numbers in the objective function | 26381836591110 |
Number of bits of the sum of numbers in the objective function | 45 |
Biggest number in a constraint | 42949672960 |
Number of bits of the biggest number in a constraint | 36 |
Biggest sum of numbers in a constraint | 26381836591110 |
Number of bits of the biggest sum of numbers | 45 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1203.32 |
Number of variables | 56400 |
Total number of constraints | 1090 |
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 | 1090 |
Minimum length of a constraint | 90 |
Maximum length of a constraint | 720 |
LAUNCH ON wulflinc13 THE 2005-09-23 16:10:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8671 boxname=wulflinc13 idbench=467 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c5a9e8be191d07f712a0a357db2fa392 /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sctap2.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sctap2.opb IDLAUNCH: 8671 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.180 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.180 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: 919512 kB Buffers: 13948 kB Cached: 82408 kB SwapCached: 0 kB Active: 49484 kB Inactive: 49800 kB HighTotal: 131008 kB HighFree: 44996 kB LowTotal: 903652 kB LowFree: 874516 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 10252 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 16:12:56 (client local time) WITH STATUS 0 IN 120.892 SECONDS stats: 8671 7 120.892 0
c This solver internally uses Chaff 2004.11.15 Simplified s UNKNOWN
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/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 21523029 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 373 2 364 364 0 9 0 [pid=7610] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-sctap2.opb [startup+10.0012 s] Raw data (loadavg): 0.86 0.93 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 2609 0 0 0 991 7 0 0 25 0 1 0 21523029 9641984 1921 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7610/statm): 2354 1921 364 364 0 1990 0 [pid=7610] vsize: 9416 Current children cumulated CPU time (s) 9.98 Current children cumulated vsize (Kb) 9416 [startup+20.0029 s] Raw data (loadavg): 0.88 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 4203 0 0 0 1987 11 0 0 25 0 1 0 21523029 15228928 2768 4294967295 134512640 135987407 3221224560 3221221872 134555852 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7610/statm): 3718 2768 364 364 0 3354 0 [pid=7610] vsize: 14872 Current children cumulated CPU time (s) 19.98 Current children cumulated vsize (Kb) 14872 [startup+30.0026 s] Raw data (loadavg): 0.90 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 4473 0 0 0 2986 12 0 0 25 0 1 0 21523029 15904768 3032 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 3883 3032 364 364 0 3519 0 [pid=7610] vsize: 15532 Current children cumulated CPU time (s) 29.98 Current children cumulated vsize (Kb) 15532 [startup+40.0022 s] Raw data (loadavg): 0.91 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 16405 0 0 0 3956 42 0 0 25 0 1 0 21523029 68214784 10587 4294967295 134512640 135987407 3221224560 3221205348 134892396 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 16654 10587 364 364 0 16290 0 [pid=7610] vsize: 66616 Current children cumulated CPU time (s) 39.98 Current children cumulated vsize (Kb) 66616 [startup+50.0029 s] Raw data (loadavg): 0.92 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 50023 0 0 0 4882 114 0 0 25 0 1 0 21523029 163373056 27496 4294967295 134512640 135987407 3221224560 3221192944 134877708 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 39886 27496 364 364 0 39522 0 [pid=7610] vsize: 159544 Current children cumulated CPU time (s) 49.96 Current children cumulated vsize (Kb) 159544 [startup+60.0026 s] Raw data (loadavg): 0.94 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 82433 0 0 0 5812 182 0 0 25 0 1 0 21523029 330985472 49945 4294967295 134512640 135987407 3221224560 3221194528 134887487 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 80807 49945 364 364 0 80443 0 [pid=7610] vsize: 323228 Current children cumulated CPU time (s) 59.94 Current children cumulated vsize (Kb) 323228 [startup+70.0032 s] Raw data (loadavg): 0.95 0.94 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 106630 0 0 0 6754 239 0 0 25 0 1 0 21523029 318664704 61599 4294967295 134512640 135987407 3221224560 3221186940 135480440 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 77799 61599 364 364 0 77435 0 [pid=7610] vsize: 311196 Current children cumulated CPU time (s) 69.93 Current children cumulated vsize (Kb) 311196 [startup+80.0039 s] Raw data (loadavg): 0.95 0.95 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 149476 0 0 0 7657 334 0 0 25 0 1 0 21523029 448229376 84799 4294967295 134512640 135987407 3221224560 3221181616 134878317 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 109431 84799 364 364 0 109067 0 [pid=7610] vsize: 437724 Current children cumulated CPU time (s) 79.91 Current children cumulated vsize (Kb) 437724 [startup+90.0035 s] Raw data (loadavg): 0.96 0.95 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 188675 0 0 0 8569 421 0 0 25 0 1 0 21523029 552947712 99171 4294967295 134512640 135987407 3221224560 3221196160 134537477 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/7610/statm): 134997 99171 364 364 0 134633 0 [pid=7610] vsize: 539988 Current children cumulated CPU time (s) 89.9 Current children cumulated vsize (Kb) 539988 [startup+100.004 s] Raw data (loadavg): 0.97 0.95 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 203283 0 0 0 9535 456 0 0 25 0 1 0 21523029 590827520 113529 4294967295 134512640 135987407 3221224560 3221211520 134878699 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7610/statm): 144245 113529 364 364 0 143881 0 [pid=7610] vsize: 576980 Current children cumulated CPU time (s) 99.91 Current children cumulated vsize (Kb) 576980 [startup+110.005 s] Raw data (loadavg): 0.97 0.95 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 220022 0 0 0 10487 502 0 0 25 0 1 0 21523029 595693568 129982 4294967295 134512640 135987407 3221224560 3221209312 134887887 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7610/statm): 145433 129982 364 364 0 145069 0 [pid=7610] vsize: 581732 Current children cumulated CPU time (s) 109.89 Current children cumulated vsize (Kb) 581732 [startup+120.005 s] Raw data (loadavg): 0.97 0.95 0.95 2/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) R 7609 7610 4060 0 -1 0 233413 0 0 0 11449 540 0 0 25 0 1 0 21523029 651567104 143152 4294967295 134512640 135987407 3221224560 3221179216 134856487 0 0 5 16384 0 0 0 17 0 0 0 Raw data (/proc/7610/statm): 159074 143153 364 364 0 158710 0 [pid=7610] vsize: 636296 Current children cumulated CPU time (s) 119.89 Current children cumulated vsize (Kb) 636296 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+120.651 s] Raw data (loadavg): 0.97 0.95 0.95 1/55 7610 Raw data (/proc/7610/stat): 7610 (pb2sat) T 7609 7610 4060 0 -1 0 237946 0 0 0 11504 549 0 0 25 0 1 0 21523029 943812608 147546 4294967295 134512640 135987407 3221224560 3221209180 135635874 0 0 5 16384 3222434794 0 0 17 0 0 0 Raw data (/proc/7610/statm): 230423 147546 364 364 0 230059 0 [pid=7610] vsize: 921692 Current children cumulated CPU time (s) 120.53 Current children cumulated vsize (Kb) 921692 Sending SIGTERM to -7610 Sleeping 2 seconds Sending SIGKILL to -7610 One traced child (pid=7610) ended because it received signal 9 (SIGKILL) All traced children have exited ! Game is over. Child ended because it received signal 9 (SIGKILL) Real time (s): 122.957 CPU time (s): 120.892 CPU user time (s): 115.1 CPU system time (s): 5.79112 CPU usage (%): 98.3203 Max. virtual memory (cumulated for all children) (Kb): 921692
ERROR: no interpretation found !