Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-siena1.opb |
MD5SUM | 575f632072d90cb1b2032661c3842261 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 70755 |
Biggest coefficient in the objective function | 536870912000000000000 |
Number of bits for the biggest coefficient in the objective function | 69 |
Sum of the numbers in the objective function | 28224865138562973040640 |
Number of bits of the sum of numbers in the objective function | 75 |
Biggest number in a constraint | 536870912000000000000 |
Number of bits of the biggest number in a constraint | 69 |
Biggest sum of numbers in a constraint | 28224967538562973040640 |
Number of bits of the biggest sum of numbers | 75 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 70755 |
Total number of constraints | 13995 |
Number of constraints which are clauses | 310 |
Number of constraints which are cardinality constraints (but not clauses) | 11776 |
Number of constraints which are nor clauses,nor cardinality constraints | 1909 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70755 |
LAUNCH ON wulflinc10 THE 2005-09-23 17:39:49 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=8973 boxname=wulflinc10 idbench=769 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 575f632072d90cb1b2032661c3842261 /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-siena1.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-siena1.opb IDLAUNCH: 8973 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.193 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.193 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: 926180 kB Buffers: 11996 kB Cached: 79124 kB SwapCached: 0 kB Active: 54172 kB Inactive: 39868 kB HighTotal: 131008 kB HighFree: 47880 kB LowTotal: 903652 kB LowFree: 878300 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6976 kB Slab: 8808 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 17:43:24 (client local time) WITH STATUS 0 IN 212.96 SECONDS stats: 8973 7 212.96 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/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22059824 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 373 2 364 364 0 9 0 [pid=8312] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-siena1.opb [startup+10.0012 s] Raw data (loadavg): 0.93 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 2481 0 0 0 991 7 0 0 25 0 1 0 22059824 9367552 1795 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 2287 1795 364 364 0 1923 0 [pid=8312] vsize: 9148 Current children cumulated CPU time (s) 9.98 Current children cumulated vsize (Kb) 9148 [startup+20.0018 s] Raw data (loadavg): 0.94 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 2994 0 0 0 1990 8 0 0 25 0 1 0 22059824 10584064 2300 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 2584 2300 364 364 0 2220 0 [pid=8312] vsize: 10336 Current children cumulated CPU time (s) 19.98 Current children cumulated vsize (Kb) 10336 [startup+30.0013 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 4375 0 0 0 2986 12 0 0 25 0 1 0 22059824 15630336 2936 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 3816 2936 364 364 0 3452 0 [pid=8312] vsize: 15264 Current children cumulated CPU time (s) 29.98 Current children cumulated vsize (Kb) 15264 [startup+40.0019 s] Raw data (loadavg): 0.96 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 4647 0 0 0 3985 13 0 0 25 0 1 0 22059824 16306176 3203 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 3981 3203 364 364 0 3617 0 [pid=8312] vsize: 15924 Current children cumulated CPU time (s) 39.98 Current children cumulated vsize (Kb) 15924 [startup+50.0024 s] Raw data (loadavg): 0.96 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 4901 0 0 0 4984 14 0 0 25 0 1 0 22059824 16982016 3453 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4146 3453 364 364 0 3782 0 [pid=8312] vsize: 16584 Current children cumulated CPU time (s) 49.98 Current children cumulated vsize (Kb) 16584 [startup+60.002 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 5131 0 0 0 5983 15 0 0 25 0 1 0 22059824 17522688 3679 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4278 3679 364 364 0 3914 0 [pid=8312] vsize: 17112 Current children cumulated CPU time (s) 59.98 Current children cumulated vsize (Kb) 17112 [startup+70.0026 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 5340 0 0 0 6983 15 0 0 25 0 1 0 22059824 18063360 3885 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4410 3885 364 364 0 4046 0 [pid=8312] vsize: 17640 Current children cumulated CPU time (s) 69.98 Current children cumulated vsize (Kb) 17640 [startup+80.0031 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 5537 0 0 0 7982 16 0 0 25 0 1 0 22059824 18604032 4079 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4542 4079 364 364 0 4178 0 [pid=8312] vsize: 18168 Current children cumulated CPU time (s) 79.98 Current children cumulated vsize (Kb) 18168 [startup+90.0037 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 5723 0 0 0 8982 16 0 0 25 0 1 0 22059824 19009536 4262 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4641 4262 364 364 0 4277 0 [pid=8312] vsize: 18564 Current children cumulated CPU time (s) 89.98 Current children cumulated vsize (Kb) 18564 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 5896 0 0 0 9981 17 0 0 25 0 1 0 22059824 19550208 4432 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 4773 4432 364 364 0 4409 0 [pid=8312] vsize: 19092 Current children cumulated CPU time (s) 99.98 Current children cumulated vsize (Kb) 19092 [startup+110.003 s] Raw data (loadavg): 0.98 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 8283 0 0 0 10975 22 0 0 25 0 1 0 22059824 28696576 5341 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 7006 5341 364 364 0 6642 0 [pid=8312] vsize: 28024 Current children cumulated CPU time (s) 109.97 Current children cumulated vsize (Kb) 28024 [startup+120.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 8342 0 0 0 11975 23 0 0 25 0 1 0 22059824 28696576 5398 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 7006 5398 364 364 0 6642 0 [pid=8312] vsize: 28024 Current children cumulated CPU time (s) 119.98 Current children cumulated vsize (Kb) 28024 [startup+130.003 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 10194 0 0 0 12969 29 0 0 25 0 1 0 22059824 34947072 6899 4294967295 134512640 135987407 3221224560 3221213104 134893007 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 8532 6899 364 364 0 8168 0 [pid=8312] vsize: 34128 Current children cumulated CPU time (s) 129.98 Current children cumulated vsize (Kb) 34128 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 41911 0 0 0 13899 97 0 0 25 0 1 0 22059824 125308928 25320 4294967295 134512640 135987407 3221224560 3221179588 135477877 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 30593 25320 364 364 0 30229 0 [pid=8312] vsize: 122372 Current children cumulated CPU time (s) 139.96 Current children cumulated vsize (Kb) 122372 [startup+150.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 77052 0 0 0 14821 173 0 0 25 0 1 0 22059824 234618880 44374 4294967295 134512640 135987407 3221224560 3221192940 135499901 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 57280 44374 364 364 0 56916 0 [pid=8312] vsize: 229120 Current children cumulated CPU time (s) 149.94 Current children cumulated vsize (Kb) 229120 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 104352 0 0 0 15756 238 0 0 25 0 1 0 22059824 322560000 59137 4294967295 134512640 135987407 3221224560 3221179560 135487877 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 78750 59137 364 364 0 78386 0 [pid=8312] vsize: 315000 Current children cumulated CPU time (s) 159.94 Current children cumulated vsize (Kb) 315000 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 131099 0 0 0 16696 295 0 0 25 0 1 0 22059824 488148992 85255 4294967295 134512640 135987407 3221224560 3221204044 135499880 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 119177 85255 364 364 0 118813 0 [pid=8312] vsize: 476708 Current children cumulated CPU time (s) 169.91 Current children cumulated vsize (Kb) 476708 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 186622 0 0 0 17577 412 0 0 25 0 1 0 22059824 556572672 96948 4294967295 134512640 135987407 3221224560 3221205248 134636939 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 135882 96948 364 364 0 135518 0 [pid=8312] vsize: 543528 Current children cumulated CPU time (s) 179.89 Current children cumulated vsize (Kb) 543528 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 201939 0 0 0 18535 454 0 0 25 0 1 0 22059824 594182144 112010 4294967295 134512640 135987407 3221224560 3221210752 134556288 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 145064 112010 364 364 0 144700 0 [pid=8312] vsize: 580256 Current children cumulated CPU time (s) 189.89 Current children cumulated vsize (Kb) 580256 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 219654 0 0 0 19491 497 0 0 25 0 1 0 22059824 599048192 129432 4294967295 134512640 135987407 3221224560 3221213200 134878604 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 146252 129432 364 364 0 145888 0 [pid=8312] vsize: 585008 Current children cumulated CPU time (s) 199.88 Current children cumulated vsize (Kb) 585008 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) R 8311 8312 4061 0 -1 0 233802 0 0 0 20458 530 0 0 25 0 1 0 22059824 653164544 143346 4294967295 134512640 135987407 3221224560 3221205340 135500004 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/8312/statm): 159464 143346 364 364 0 159100 0 [pid=8312] vsize: 637856 Current children cumulated CPU time (s) 209.88 Current children cumulated vsize (Kb) 637856 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+212.685 s] Raw data (loadavg): 0.99 0.97 0.92 1/55 8312 Raw data (/proc/8312/stat): 8312 (pb2sat) T 8311 8312 4061 0 -1 0 240572 0 0 0 20710 545 0 0 25 0 1 0 22059824 943788032 149963 4294967295 134512640 135987407 3221224560 3221206460 135635874 0 0 5 16384 3222434794 0 0 17 1 0 0 Raw data (/proc/8312/statm): 230417 149963 364 364 0 230053 0 [pid=8312] vsize: 921668 Current children cumulated CPU time (s) 212.55 Current children cumulated vsize (Kb) 921668 Sending SIGTERM to -8312 Sleeping 2 seconds Sending SIGKILL to -8312 One traced child (pid=8312) 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): 214.995 CPU time (s): 212.96 CPU user time (s): 207.198 CPU system time (s): 5.76112 CPU usage (%): 99.0532 Max. virtual memory (cumulated for all children) (Kb): 921668
ERROR: no interpretation found !