Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-dc1l.opb |
MD5SUM | 5b92932a8bc350218da666e6f064f13f |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 57964723104641792 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 68818 |
Biggest coefficient in the objective function | 524288000000000000 |
Number of bits for the biggest coefficient in the objective function | 59 |
Sum of the numbers in the objective function | 6652856940207324781 |
Number of bits of the sum of numbers in the objective function | 63 |
Biggest number in a constraint | 524288000000000000 |
Number of bits of the biggest number in a constraint | 59 |
Biggest sum of numbers in a constraint | 6652856940207324781 |
Number of bits of the biggest sum of numbers | 63 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1205.91 |
Number of variables | 68678 |
Total number of constraints | 37291 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 35639 |
Number of constraints which are nor clauses,nor cardinality constraints | 1652 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 35119 |
LAUNCH ON wulflinc3 THE 2005-09-23 19:13:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=9349 boxname=wulflinc3 idbench=1145 idsolver=8 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5b92932a8bc350218da666e6f064f13f /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-dc1l.opb REAL COMMAND: pb2sat /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-dc1l.opb IDLAUNCH: 9349 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.228 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.228 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: 906028 kB Buffers: 13908 kB Cached: 97136 kB SwapCached: 0 kB Active: 56044 kB Inactive: 57932 kB HighTotal: 131008 kB HighFree: 29512 kB LowTotal: 903652 kB LowFree: 876516 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6980 kB Slab: 9048 kB Committed_AS: 63660 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-23 19:17:06 (client local time) WITH STATUS 0 IN 217.99 SECONDS stats: 9349 7 217.99 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/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 18 0 0 0 0 0 0 0 23 0 1 0 22636294 1527808 2 4294967295 134512640 135987407 3221224560 3221224560 134512928 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 373 2 364 364 0 9 0 [pid=10986] vsize: 1492 open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-dc1l.opb [startup+10.0028 s] Raw data (loadavg): 0.93 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 2317 0 0 0 992 5 0 0 25 0 1 0 22636294 8962048 1634 4294967295 134512640 135987407 3221224560 3221221744 134536160 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 2188 1634 364 364 0 1824 0 [pid=10986] vsize: 8752 Current children cumulated CPU time (s) 9.97 Current children cumulated vsize (Kb) 8752 [startup+20.0036 s] Raw data (loadavg): 0.94 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 2907 0 0 0 1990 7 0 0 25 0 1 0 22636294 10448896 2214 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 2551 2214 364 364 0 2187 0 [pid=10986] vsize: 10204 Current children cumulated CPU time (s) 19.97 Current children cumulated vsize (Kb) 10204 [startup+30.0035 s] Raw data (loadavg): 0.95 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 4312 0 0 0 2987 10 0 0 25 0 1 0 22636294 15495168 2874 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 3783 2874 364 364 0 3419 0 [pid=10986] vsize: 15132 Current children cumulated CPU time (s) 29.97 Current children cumulated vsize (Kb) 15132 [startup+40.0043 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 4585 0 0 0 3986 11 0 0 25 0 1 0 22636294 16035840 3142 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 3915 3142 364 364 0 3551 0 [pid=10986] vsize: 15660 Current children cumulated CPU time (s) 39.97 Current children cumulated vsize (Kb) 15660 [startup+50.0051 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 4848 0 0 0 4985 12 0 0 25 0 1 0 22636294 16711680 3401 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4080 3401 364 364 0 3716 0 [pid=10986] vsize: 16320 Current children cumulated CPU time (s) 49.97 Current children cumulated vsize (Kb) 16320 [startup+60.006 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 5085 0 0 0 5984 13 0 0 25 0 1 0 22636294 17387520 3634 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4245 3634 364 364 0 3881 0 [pid=10986] vsize: 16980 Current children cumulated CPU time (s) 59.97 Current children cumulated vsize (Kb) 16980 [startup+70.0058 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 5300 0 0 0 6983 14 0 0 25 0 1 0 22636294 17928192 3845 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4377 3845 364 364 0 4013 0 [pid=10986] vsize: 17508 Current children cumulated CPU time (s) 69.97 Current children cumulated vsize (Kb) 17508 [startup+80.0056 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 5500 0 0 0 7982 15 0 0 25 0 1 0 22636294 18468864 4042 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4509 4042 364 364 0 4145 0 [pid=10986] vsize: 18036 Current children cumulated CPU time (s) 79.97 Current children cumulated vsize (Kb) 18036 [startup+90.0065 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 5685 0 0 0 8982 15 0 0 25 0 1 0 22636294 18874368 4224 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4608 4224 364 364 0 4244 0 [pid=10986] vsize: 18432 Current children cumulated CPU time (s) 89.97 Current children cumulated vsize (Kb) 18432 [startup+100.006 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 5862 0 0 0 9981 16 0 0 25 0 1 0 22636294 19415040 4398 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 4740 4398 364 364 0 4376 0 [pid=10986] vsize: 18960 Current children cumulated CPU time (s) 99.97 Current children cumulated vsize (Kb) 18960 [startup+110.007 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 8259 0 0 0 10976 21 0 0 25 0 1 0 22636294 28696576 5318 4294967295 134512640 135987407 3221224560 3221221872 134555859 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 7006 5318 364 364 0 6642 0 [pid=10986] vsize: 28024 Current children cumulated CPU time (s) 109.97 Current children cumulated vsize (Kb) 28024 [startup+120.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 8319 0 0 0 11975 21 0 0 25 0 1 0 22636294 28696576 5375 4294967295 134512640 135987407 3221224560 3221221872 134555861 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 7006 5375 364 364 0 6642 0 [pid=10986] vsize: 28024 Current children cumulated CPU time (s) 119.96 Current children cumulated vsize (Kb) 28024 [startup+130.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 28082 0 0 0 12928 67 0 0 25 0 1 0 22636294 85520384 16463 4294967295 134512640 135987407 3221224560 3221150608 134855001 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 20879 16463 364 364 0 20515 0 [pid=10986] vsize: 83516 Current children cumulated CPU time (s) 129.95 Current children cumulated vsize (Kb) 83516 [startup+140.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 56754 0 0 0 13866 128 0 0 25 0 1 0 22636294 179159040 33919 4294967295 134512640 135987407 3221224560 3221208448 134856570 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 43740 33919 364 364 0 43376 0 [pid=10986] vsize: 174960 Current children cumulated CPU time (s) 139.94 Current children cumulated vsize (Kb) 174960 [startup+150.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 95975 0 0 0 14786 206 0 0 25 0 1 0 22636294 295800832 50941 4294967295 134512640 135987407 3221224560 3221093648 134537491 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 72217 50941 364 364 0 71853 0 [pid=10986] vsize: 288868 Current children cumulated CPU time (s) 149.92 Current children cumulated vsize (Kb) 288868 [startup+160.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 110697 0 0 0 15755 236 0 0 25 0 1 0 22636294 338546688 65444 4294967295 134512640 135987407 3221224560 3221126076 135500006 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 82653 65444 364 364 0 82289 0 [pid=10986] vsize: 330612 Current children cumulated CPU time (s) 159.91 Current children cumulated vsize (Kb) 330612 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 131639 0 0 0 16715 275 0 0 25 0 1 0 22636294 497782784 85912 4294967295 134512640 135987407 3221224560 3221113292 135500004 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 121529 85912 364 364 0 121165 0 [pid=10986] vsize: 486116 Current children cumulated CPU time (s) 169.9 Current children cumulated vsize (Kb) 486116 [startup+180.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 188400 0 0 0 17597 389 0 0 25 0 1 0 22636294 571072512 98762 4294967295 134512640 135987407 3221224560 3221073148 134636966 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 139422 98762 364 364 0 139058 0 [pid=10986] vsize: 557688 Current children cumulated CPU time (s) 179.86 Current children cumulated vsize (Kb) 557688 [startup+190.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 200956 0 0 0 18571 416 0 0 25 0 1 0 22636294 607330304 111109 4294967295 134512640 135987407 3221224560 3221216124 135499901 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 148274 111109 364 364 0 147910 0 [pid=10986] vsize: 593096 Current children cumulated CPU time (s) 189.87 Current children cumulated vsize (Kb) 593096 [startup+200.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 216851 0 0 0 19532 454 0 0 25 0 1 0 22636294 610979840 126740 4294967295 134512640 135987407 3221224560 3221187784 134636945 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 149165 126740 364 364 0 148801 0 [pid=10986] vsize: 596660 Current children cumulated CPU time (s) 199.86 Current children cumulated vsize (Kb) 596660 [startup+210.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 0 229904 0 0 0 20502 484 0 0 25 0 1 0 22636294 665096192 139580 4294967295 134512640 135987407 3221224560 3221185280 134878092 0 0 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 162377 139580 364 364 0 162013 0 [pid=10986] vsize: 649508 Current children cumulated CPU time (s) 209.86 Current children cumulated vsize (Kb) 649508 Mem limit exceeded: sending SIGTERM then SIGKILL [startup+217.74 s] Raw data (loadavg): 0.99 0.97 0.91 1/55 10986 Raw data (/proc/10986/stat): 10986 (pb2sat) T 10985 10986 4060 0 -1 0 242978 0 0 0 21243 515 0 0 25 0 1 0 22636294 956665856 152451 4294967295 134512640 135987407 3221224560 3221189104 135544035 0 0 5 16384 3222434794 0 0 17 1 0 0 Raw data (/proc/10986/statm): 233561 152451 364 364 0 233197 0 [pid=10986] vsize: 934244 Current children cumulated CPU time (s) 217.58 Current children cumulated vsize (Kb) 934244 Sending SIGTERM to -10986 Sleeping 2 seconds Sending SIGKILL to -10986 [startup+220.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 10987 Raw data (/proc/10986/stat): 10986 (pb2sat) R 10985 10986 4060 0 -1 1028 242979 0 0 0 21252 542 0 0 18 0 1 0 22636294 0 0 4294967295 0 0 0 0 0 0 16384 5 16384 0 0 0 17 1 0 0 Raw data (/proc/10986/statm): 0 0 0 0 0 0 0 [pid=10986] vsize: 0 Current children cumulated CPU time (s) 217.94 Current children cumulated vsize (Kb) 0 One traced child (pid=10986) 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): 220.056 CPU time (s): 217.99 CPU user time (s): 212.526 CPU system time (s): 5.46417 CPU usage (%): 99.0609 Max. virtual memory (cumulated for all children) (Kb): 934244
ERROR: no interpretation found !