Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl10_15_pb.cnf.cr.opb |
MD5SUM | ba9cd165dfff9daff67f98334a7b589e |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 16 |
Number of bits of the biggest sum of numbers | 5 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.009997 |
Number of variables | 300 |
Total number of constraints | 50 |
Number of constraints which are clauses | 30 |
Number of constraints which are cardinality constraints (but not clauses) | 20 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 10 |
Maximum length of a constraint | 15 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-06-07 07:10:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=27445 boxname=wulflinc5 idbench=3 idsolver=20 numberseed=0 MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048 /oldhome/oroussel/solvers/bsolo_lpr-v2 MD5SUM BENCH: ba9cd165dfff9daff67f98334a7b589e /oldhome/oroussel/tmp/wulflinc5/normalized-chnl10_15_pb.cnf.cr.opb REAL COMMAND: bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc5/normalized-chnl10_15_pb.cnf.cr.opb IDLAUNCH: 27445 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 351400 kB Buffers: 34220 kB Cached: 624676 kB SwapCached: 568 kB Active: 54988 kB Inactive: 605956 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 351148 kB SwapTotal: 2097136 kB SwapFree: 2095632 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5156 kB Slab: 16756 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-07 07:14:59 (client local time) WITH STATUS 20 IN 257.073 SECONDS stats: 27445 7 257.073 20 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c INFO: No cost function. Find solution and finish. c Initial problem consists of 300 variables and 50 constraints. c After prepocess the problem consists of 300 variables and 50 constraints. c preprocess terminated 0.084 s c Not use computed LB before first solution. s UNSATISFIABLE c Exit Code: 20 c Total time: 257.04 s #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.00 0.00 0.00 2/54 2519 Raw data (stat): 2519 (runsolver) R 2518 7266 7265 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 891087486 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0004 s] Raw data (loadavg): 0.15 0.03 0.01 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 2283 0 15 0 955 7 0 0 25 0 1 0 891087486 12509184 2216 4294967295 134512640 134716908 3221224576 3221223168 134549689 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 3054 2216 1111 63 0 2991 0 vsize: 12216 [startup+20.0013 s] Raw data (loadavg): 0.28 0.06 0.02 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 2953 0 15 0 1952 10 0 0 25 0 1 0 891087486 15237120 2886 4294967295 134512640 134716908 3221224576 3221223360 134529404 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 3720 2886 1111 63 0 3657 0 vsize: 14880 [startup+30.0091 s] Raw data (loadavg): 0.39 0.09 0.03 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 4053 0 15 0 2949 14 0 0 25 0 1 0 891087486 19853312 3985 4294967295 134512640 134716908 3221224576 3221223168 134549697 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 4847 3985 1111 63 0 4784 0 vsize: 19388 [startup+40.0098 s] Raw data (loadavg): 0.49 0.12 0.04 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 4936 0 15 0 3946 18 0 0 25 0 1 0 891087486 23523328 4868 4294967295 134512640 134716908 3221224576 3221223144 1077378037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 5743 4868 1111 63 0 5680 0 vsize: 22972 [startup+50.0106 s] Raw data (loadavg): 0.56 0.15 0.05 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 5468 0 15 0 4943 20 0 0 25 0 1 0 891087486 25706496 5397 4294967295 134512640 134716908 3221224576 3221223256 134552633 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6276 5397 1111 63 0 6213 0 vsize: 25104 [startup+60.0113 s] Raw data (loadavg): 0.63 0.18 0.06 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 5976 0 15 0 5941 22 0 0 25 0 1 0 891087486 27766784 5905 4294967295 134512640 134716908 3221224576 3221223232 134536638 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 6779 5905 1111 63 0 6716 0 vsize: 27116 [startup+70.012 s] Raw data (loadavg): 0.69 0.21 0.07 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 6648 0 15 0 6939 25 0 0 25 0 1 0 891087486 30633984 6574 4294967295 134512640 134716908 3221224576 3221223280 134528650 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7479 6574 1111 63 0 7416 0 vsize: 29916 [startup+80.0127 s] Raw data (loadavg): 0.73 0.23 0.08 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 7133 0 15 0 7937 27 0 0 25 0 1 0 891087486 32563200 7059 4294967295 134512640 134716908 3221224576 3221223144 1077378037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 7950 7059 1111 63 0 7887 0 vsize: 31800 [startup+90.0134 s] Raw data (loadavg): 0.77 0.26 0.09 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 7443 0 15 0 8936 28 0 0 25 0 1 0 891087486 33943552 7366 4294967295 134512640 134716908 3221224576 3221223152 134549802 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8287 7366 1111 63 0 8224 0 vsize: 33148 [startup+100.013 s] Raw data (loadavg): 0.81 0.28 0.10 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 7949 0 15 0 9935 30 0 0 25 0 1 0 891087486 36114432 7871 4294967295 134512640 134716908 3221224576 3221223232 134536638 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 8817 7871 1111 63 0 8754 0 vsize: 35268 [startup+110.014 s] Raw data (loadavg): 0.84 0.30 0.11 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 8412 0 15 0 10933 32 0 0 25 0 1 0 891087486 38035456 8334 4294967295 134512640 134716908 3221224576 3221223168 134549689 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9286 8334 1111 63 0 9223 0 vsize: 37144 [startup+120.015 s] Raw data (loadavg): 0.86 0.33 0.12 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 8728 0 15 0 11933 32 0 0 25 0 1 0 891087486 39256064 8649 4294967295 134512640 134716908 3221224576 3221223168 134549689 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9584 8649 1111 63 0 9521 0 vsize: 38336 [startup+130.015 s] Raw data (loadavg): 0.88 0.35 0.12 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 9034 0 15 0 12932 34 0 0 25 0 1 0 891087486 40607744 8955 4294967295 134512640 134716908 3221224576 3221223216 134536655 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 9914 8955 1111 63 0 9851 0 vsize: 39656 [startup+140.016 s] Raw data (loadavg): 0.90 0.37 0.13 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 9254 0 15 0 13932 34 0 0 25 0 1 0 891087486 41463808 9174 4294967295 134512640 134716908 3221224576 3221223244 134536852 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10123 9174 1111 63 0 10060 0 vsize: 40492 [startup+150.017 s] Raw data (loadavg): 0.92 0.39 0.14 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 9596 0 15 0 14930 36 0 0 25 0 1 0 891087486 43008000 9511 4294967295 134512640 134716908 3221224576 3221223220 134536649 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10500 9511 1111 63 0 10437 0 vsize: 42000 [startup+160.018 s] Raw data (loadavg): 0.93 0.41 0.15 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 9874 0 15 0 15929 38 0 0 25 0 1 0 891087486 44089344 9789 4294967295 134512640 134716908 3221224576 3221223228 134536828 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10764 9789 1111 63 0 10701 0 vsize: 43056 [startup+170.018 s] Raw data (loadavg): 0.94 0.43 0.16 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 10061 0 15 0 16928 38 0 0 25 0 1 0 891087486 44933120 9976 4294967295 134512640 134716908 3221224576 3221223068 134552632 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 10970 9976 1111 63 0 10907 0 vsize: 43880 [startup+180.019 s] Raw data (loadavg): 0.95 0.45 0.17 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 10223 0 15 0 17928 39 0 0 25 0 1 0 891087486 45645824 10136 4294967295 134512640 134716908 3221224576 3221223360 134529091 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11144 10136 1111 63 0 11081 0 vsize: 44576 [startup+190.02 s] Raw data (loadavg): 0.95 0.46 0.18 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 10429 0 15 0 18927 40 0 0 25 0 1 0 891087486 46493696 10340 4294967295 134512640 134716908 3221224576 3221223228 134536817 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11351 10340 1111 63 0 11288 0 vsize: 45404 [startup+200.019 s] Raw data (loadavg): 0.96 0.48 0.19 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 10689 0 15 0 19927 40 0 0 25 0 1 0 891087486 47706112 10595 4294967295 134512640 134716908 3221224576 3221223220 134523868 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11647 10595 1111 63 0 11584 0 vsize: 46588 [startup+210.02 s] Raw data (loadavg): 0.97 0.50 0.19 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 10890 0 15 0 20926 41 0 0 25 0 1 0 891087486 48381952 10796 4294967295 134512640 134716908 3221224576 3221223168 134549764 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11812 10796 1111 63 0 11749 0 vsize: 47248 [startup+220.021 s] Raw data (loadavg): 0.97 0.51 0.20 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 11058 0 15 0 21925 42 0 0 25 0 1 0 891087486 49094656 10964 4294967295 134512640 134716908 3221224576 3221223312 134523930 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 11986 10964 1111 63 0 11923 0 vsize: 47944 [startup+230.022 s] Raw data (loadavg): 0.98 0.53 0.21 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 11202 0 15 0 22925 43 0 0 25 0 1 0 891087486 49827840 11104 4294967295 134512640 134716908 3221224576 3221223360 134529091 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12165 11104 1111 63 0 12102 0 vsize: 48660 [startup+240.022 s] Raw data (loadavg): 0.98 0.54 0.22 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 11378 0 15 0 23924 44 0 0 25 0 1 0 891087486 50556928 11276 4294967295 134512640 134716908 3221224576 3221223344 134529376 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12343 11276 1111 63 0 12280 0 vsize: 49372 [startup+250.022 s] Raw data (loadavg): 0.98 0.56 0.22 2/54 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 11557 0 15 0 24924 44 0 0 25 0 1 0 891087486 51388416 11450 4294967295 134512640 134716908 3221224576 3221223144 1077378037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12546 11450 1111 63 0 12483 0 vsize: 50184 [startup+257.404 s] Raw data (loadavg): 0.98 0.57 0.23 1/53 2519 Raw data (stat): 2519 (bsolo_lpr-v2) R 2518 7266 7265 0 -1 0 11557 0 15 0 24924 44 0 0 25 0 1 0 891087486 51388416 11450 4294967295 134512640 134716908 3221224576 3221223144 1077378037 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 12546 11450 1111 63 0 12483 0 vsize: 0 Child status: 20 Real time (s): 257.403 CPU time (s): 257.073 CPU user time (s): 256.6 CPU system time (s): 0.472928 CPU usage (%): 99.8716 Max. virtual memory (Kb): 50184 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####