Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-pipex.opb |
MD5SUM | b9c1029cc1d97a8d60e984f96f5d3267 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 788263 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 48 |
Biggest coefficient in the objective function | 107865 |
Number of bits for the biggest coefficient in the objective function | 17 |
Sum of the numbers in the objective function | 2514082 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 107865 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 2514082 |
Number of bits of the biggest sum of numbers | 22 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 48 |
Total number of constraints | 73 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 64 |
Number of constraints which are nor clauses,nor cardinality constraints | 9 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-04-22 01:53:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12204 boxname=wulflinc3 idbench=939 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b9c1029cc1d97a8d60e984f96f5d3267 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-pipex.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-pipex.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-pipex.opb IDLAUNCH: 12204 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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: 491756 kB Buffers: 34516 kB Cached: 486228 kB SwapCached: 0 kB Active: 45204 kB Inactive: 478276 kB HighTotal: 131008 kB HighFree: 27048 kB LowTotal: 903652 kB LowFree: 464708 kB SwapTotal: 2097136 kB SwapFree: 2096992 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6844 kB Slab: 13688 kB Committed_AS: 71776 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 01:57:20 (client local time) WITH STATUS 30 IN 218.627 SECONDS stats: 12204 0 218.627 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 41 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################ c -- Clauses(.)/Splits(s): (none) c ---[ 40]---> Adder-cost: 80 maxlim: 183 bits: 9/8 c ---[ 39]---> Adder-cost: 80 maxlim: 158 bits: 9/8 c ---[ 38]---> Adder-cost: 80 maxlim: 148 bits: 9/8 c ---[ 37]---> Adder-cost: 27 maxlim: 170 bits: 9/8 c ---[ 36]---> Adder-cost: 27 maxlim: 145 bits: 9/8 c ---[ 35]---> Adder-cost: 27 maxlim: 135 bits: 9/8 c ---[ 34]---> Adder-cost: 97 maxlim: 1468 bits: 11/11 c ---[ 33]---> Adder-cost: 97 maxlim: 1218 bits: 11/11 c ---[ 32]---> Adder-cost: 97 maxlim: 1118 bits: 11/11 c ---[ 30]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 28]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 26]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 24]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 22]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 20]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 18]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 16]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 14]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 12]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 10]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 8]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 6]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 4]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 2]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ---[ 0]---> Adder-cost: 2 maxlim: 2 bits: 2/2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 4159 14878 | 1386 0 0 nan | 0.000 % | c | 104 | 4159 14878 | 1524 104 699 6.7 | 12.316 % | c | 254 | 4159 14878 | 1677 254 2186 8.6 | 12.316 % | c | 479 | 4159 14878 | 1844 479 6124 12.8 | 12.316 % | c | 817 | 4159 14878 | 2029 817 11817 14.5 | 12.316 % | c | 1325 | 4159 14878 | 2232 1325 21570 16.3 | 12.316 % | c ============================================================================== c [1mFound solution: 836614[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 648 maxlim: 1677468 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1700 | 8587 30721 | 2862 1700 27652 16.3 | 12.316 % | c | 1800 | 8587 30721 | 3148 1800 29503 16.4 | 7.326 % | c | 1951 | 8587 30721 | 3463 1951 31641 16.2 | 7.326 % | c | 2176 | 8587 30721 | 3809 2176 35598 16.4 | 7.326 % | c | 2513 | 8587 30721 | 4190 2512 40428 16.1 | 7.397 % | c | 3021 | 8580 30698 | 4609 3017 52083 17.3 | 7.397 % | c | 3781 | 8580 30698 | 5070 3777 64158 17.0 | 7.397 % | c | 4921 | 8574 30681 | 5577 4916 84570 17.2 | 7.468 % | c ============================================================================== c [1mFound solution: 833939[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1680143 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5132 | 8585 30759 | 2861 5127 88845 17.3 | 7.468 % | c | 5232 | 8585 30759 | 3147 2664 37875 14.2 | 7.725 % | c | 5383 | 8585 30759 | 3461 2815 40572 14.4 | 7.725 % | c ============================================================================== c [1mFound solution: 831884[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1682198 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5464 | 8598 30904 | 2866 2896 42405 14.6 | 7.725 % | c | 5565 | 8598 30904 | 3152 2997 44599 14.9 | 8.169 % | c | 5715 | 8598 30904 | 3467 3147 49261 15.7 | 8.169 % | c ============================================================================== c [1mFound solution: 828516[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1685566 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5774 | 8612 31070 | 2870 3206 50493 15.7 | 8.169 % | c | 5875 | 8612 31070 | 3157 1704 23275 13.7 | 8.671 % | c | 6025 | 8612 31070 | 3472 1854 25702 13.9 | 8.671 % | c | 6250 | 8612 31070 | 3819 2079 29977 14.4 | 8.671 % | c | 6588 | 8612 31070 | 4201 2417 37484 15.5 | 8.671 % | c | 7095 | 8612 31070 | 4622 2924 48020 16.4 | 8.671 % | c | 7854 | 8612 31070 | 5084 3683 63082 17.1 | 8.671 % | c ============================================================================== c [1mFound solution: 816945[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1697137 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8777 | 8630 31231 | 2876 4606 80773 17.5 | 8.671 % | c | 8878 | 8630 31231 | 3163 2404 36006 15.0 | 9.179 % | c | 9029 | 8630 31231 | 3479 2555 38657 15.1 | 9.179 % | c | 9254 | 8630 31231 | 3827 2780 46369 16.7 | 9.179 % | c | 9592 | 8630 31231 | 4210 3118 54154 17.4 | 9.179 % | c ============================================================================== c [1mFound solution: 804539[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1709543 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9779 | 8644 31367 | 2881 3305 57719 17.5 | 9.179 % | c | 9882 | 8644 31367 | 3169 1756 27197 15.5 | 9.669 % | c | 10032 | 8644 31367 | 3486 1906 29499 15.5 | 9.669 % | c | 10258 | 8644 31367 | 3834 2132 32898 15.4 | 9.669 % | c | 10595 | 8644 31367 | 4218 2469 38076 15.4 | 9.669 % | c | 11102 | 8644 31367 | 4639 2976 47287 15.9 | 9.669 % | c | 11862 | 8644 31367 | 5103 3736 59608 16.0 | 9.669 % | c ============================================================================== c [1mFound solution: 800174[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1713908 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12840 | 8658 31528 | 2886 4714 87901 18.6 | 9.669 % | c | 12941 | 8658 31528 | 3174 2458 43918 17.9 | 10.192 % | c | 13092 | 8658 31528 | 3492 2609 46301 17.7 | 10.192 % | c | 13318 | 8658 31528 | 3841 2835 52434 18.5 | 10.192 % | c | 13655 | 8658 31528 | 4225 3172 58832 18.5 | 10.192 % | c | 14161 | 8658 31528 | 4647 3678 69425 18.9 | 10.192 % | c | 14920 | 8658 31528 | 5112 4437 89171 20.1 | 10.192 % | c | 16061 | 8658 31528 | 5623 2914 52995 18.2 | 10.192 % | c | 17772 | 8658 31528 | 6186 4625 80777 17.5 | 10.192 % | c | 20338 | 8658 31528 | 6805 3992 73402 18.4 | 10.192 % | c ============================================================================== c [1mFound solution: 794954[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1719128 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21045 | 8672 31670 | 2890 4699 89962 19.1 | 10.192 % | c | 21145 | 8672 31670 | 3179 2450 35728 14.6 | 10.637 % | c | 21297 | 8672 31670 | 3496 2602 37934 14.6 | 10.637 % | c | 21522 | 8672 31670 | 3846 2827 42434 15.0 | 10.637 % | c | 21859 | 8672 31670 | 4231 3164 50893 16.1 | 10.637 % | c | 22365 | 8672 31670 | 4654 3670 66063 18.0 | 10.637 % | c | 23124 | 8672 31670 | 5119 4429 85107 19.2 | 10.637 % | c | 24264 | 8672 31670 | 5631 2919 60613 20.8 | 10.637 % | c | 25972 | 8672 31670 | 6194 4627 90789 19.6 | 10.637 % | c | 28536 | 8672 31670 | 6814 3960 68299 17.2 | 10.637 % | c | 32380 | 8667 31654 | 7495 4296 85112 19.8 | 10.705 % | c | 38147 | 8667 31654 | 8245 6209 144894 23.3 | 10.705 % | c | 46799 | 8667 31654 | 9070 6358 116052 18.3 | 10.705 % | c ============================================================================== c [1mFound solution: 794030[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1720052 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53318 | 8681 31803 | 2893 8215 179184 21.8 | 10.705 % | c | 53418 | 8681 31803 | 3182 2154 35542 16.5 | 11.141 % | c | 53569 | 8681 31803 | 3500 2305 38460 16.7 | 11.141 % | c | 53797 | 8681 31803 | 3850 2533 42840 16.9 | 11.141 % | c | 54134 | 8681 31803 | 4235 2870 50789 17.7 | 11.141 % | c | 54642 | 8681 31803 | 4659 3378 61598 18.2 | 11.141 % | c | 55401 | 8681 31803 | 5125 4137 75716 18.3 | 11.141 % | c | 56542 | 8681 31803 | 5637 5278 100659 19.1 | 11.141 % | c | 58250 | 8681 31803 | 6201 4050 79810 19.7 | 11.141 % | c | 60812 | 8681 31803 | 6821 3413 57654 16.9 | 11.141 % | c | 64657 | 8681 31803 | 7503 3724 71147 19.1 | 11.141 % | c | 70423 | 8681 31803 | 8254 5631 182637 32.4 | 11.141 % | c | 79075 | 8681 31803 | 9079 5785 113878 19.7 | 11.141 % | c ============================================================================== c [1mFound solution: 788385[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1725697 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 81878 | 8689 31877 | 2896 8588 173044 20.1 | 11.141 % | c | 81978 | 8689 31877 | 3185 2247 30844 13.7 | 11.415 % | c | 82128 | 8689 31877 | 3504 2397 33009 13.8 | 11.415 % | c | 82353 | 8689 31877 | 3854 2622 36659 14.0 | 11.415 % | c | 82691 | 8689 31877 | 4240 2960 40960 13.8 | 11.415 % | c | 83197 | 8689 31877 | 4664 3466 49492 14.3 | 11.415 % | c | 83956 | 8689 31877 | 5130 4225 62701 14.8 | 11.415 % | c | 85095 | 8689 31877 | 5643 5364 83448 15.6 | 11.415 % | c | 86803 | 8689 31877 | 6207 4154 61632 14.8 | 11.415 % | c | 89367 | 8689 31877 | 6828 3501 55264 15.8 | 11.415 % | c | 93212 | 8689 31877 | 7511 3812 80448 21.1 | 11.415 % | c | 98978 | 8689 31877 | 8262 5690 113444 19.9 | 11.415 % | c | 107630 | 8689 31877 | 9088 5858 151764 25.9 | 11.415 % | c | 120606 | 8689 31877 | 9997 4833 90610 18.7 | 11.415 % | c ============================================================================== c [1mFound solution: 788263[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 1725819 bits: 22/21 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 126766 | 8699 31979 | 2899 5884 87757 14.9 | 11.415 % | c | 126869 | 8699 31979 | 3188 3045 38274 12.6 | 11.671 % | c | 127019 | 8699 31979 | 3507 3195 40214 12.6 | 11.671 % | c | 127245 | 8699 31979 | 3858 3421 44081 12.9 | 11.671 % | c | 127584 | 8699 31979 | 4244 3760 49062 13.0 | 11.671 % | c | 128090 | 8699 31979 | 4668 4266 63238 14.8 | 11.671 % | c | 128849 | 8699 31979 | 5135 2568 42193 16.4 | 11.671 % | c | 129988 | 8699 31979 | 5649 3707 76126 20.5 | 11.671 % | c | 131696 | 8699 31979 | 6214 5415 106885 19.7 | 11.671 % | c | 134259 | 8699 31979 | 6835 4768 70173 14.7 | 11.671 % | c | 138103 | 8699 31979 | 7519 5069 113971 22.5 | 11.671 % | c | 143870 | 8699 31979 | 8271 6958 173929 25.0 | 11.671 % | c | 152519 | 8699 31979 | 9098 7111 127489 17.9 | 11.671 % | c | 165494 | 8699 31979 | 10008 6091 86120 14.1 | 11.671 % | c | 184955 | 8699 31979 | 11008 10207 206230 20.2 | 11.671 % | c | 214147 | 8699 31979 | 12109 11297 273419 24.2 | 11.671 % | c | 257936 | 8699 31979 | 13320 11803 272811 23.1 | 11.671 % | c ============================================================================== c [1mOptimal solution: 788263[0m s OPTIMUM FOUND v QUAN0101_bit0 QUAN0102_bit0 -QUAN0103_bit0 -QUAN0104_bit0 -QUAN0105_bit0 -QUAN0106_bit0 -QUAN0107_bit0 -QUAN0108_bit0 -QUAN0109_bit0 -QUAN0110_bit0 QUAN0111_bit0 -QUAN0112_bit0 QUAN0113_bit0 -QUAN0114_bit0 -QUAN0115_bit0 -QUAN0116_bit0 -QUAN0201_bit0 -QUAN0202_bit0 -QUAN0203_bit0 -QUAN0204_bit0 -QUAN0205_bit0 -QUAN0206_bit0 QUAN0207_bit0 QUAN0208_bit0 -QUAN0209_bit0 -QUAN0210_bit0 -QUAN0211_bit0 QUAN0212_bit0 -QUAN0213_bit0 QUAN0214_bit0 QUAN0215_bit0 QUAN0216_bit0 -QUAN0301_bit0 -QUAN0302_bit0 QUAN0303_bit0 QUAN0304_bit0 QUAN0305_bit0 QUAN0306_bit0 -QUAN0307_bit0 -QUAN0308_bit0 QUAN0309_bit0 QUAN0310_bit0 -QUAN0311_bit0 -QUAN0312_bit0 -QUAN0313_bit0 -QUAN0314_bit0 -QUAN0315_bit0 -QUAN0316_bit0 c _______________________________________________________________________________ c c restarts : 106 c conflicts : 292581 (1339 /sec) c decisions : 369201 (1689 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 218.573 s c _______________________________________________________________________________ #### 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 Raw data (loadavg): 0.88 0.93 0.90 2/54 24699 Raw data (stat): 24699 (runsolver) R 24698 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491687351 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99995 s] Raw data (loadavg): 0.90 0.93 0.90 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 680 0 0 0 996 1 0 0 25 0 1 0 491687351 4308992 658 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1052 658 603 41 0 1011 0 vsize: 4208 [startup+19.9999 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 762 0 0 0 1996 1 0 0 25 0 1 0 491687351 4718592 740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1152 740 603 41 0 1111 0 vsize: 4608 [startup+30.001 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 805 0 0 0 2996 2 0 0 25 0 1 0 491687351 4898816 783 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1196 783 603 41 0 1155 0 vsize: 4784 [startup+40.0002 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 818 0 0 0 3995 2 0 0 25 0 1 0 491687351 4898816 796 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1196 796 603 41 0 1155 0 vsize: 4784 [startup+50.0014 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 897 0 0 0 4995 2 0 0 25 0 1 0 491687351 5300224 875 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 875 603 41 0 1253 0 vsize: 5176 [startup+60.0019 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 902 0 0 0 5995 3 0 0 25 0 1 0 491687351 5300224 880 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1294 880 603 41 0 1253 0 vsize: 5176 [startup+70.0017 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 902 0 0 0 6994 3 0 0 25 0 1 0 491687351 5300224 880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 880 603 41 0 1253 0 vsize: 5176 [startup+80.0029 s] Raw data (loadavg): 0.97 0.94 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 910 0 0 0 7994 3 0 0 25 0 1 0 491687351 5300224 888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 888 603 41 0 1253 0 vsize: 5176 [startup+90.0027 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 913 0 0 0 8994 3 0 0 25 0 1 0 491687351 5300224 891 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 891 603 41 0 1253 0 vsize: 5176 [startup+100.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 919 0 0 0 9994 3 0 0 25 0 1 0 491687351 5300224 897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 897 603 41 0 1253 0 vsize: 5176 [startup+110.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 922 0 0 0 10994 3 0 0 25 0 1 0 491687351 5300224 900 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1294 900 603 41 0 1253 0 vsize: 5176 [startup+120.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 941 0 0 0 11994 3 0 0 25 0 1 0 491687351 5431296 919 4294967295 134512640 134672761 3221224544 3221223728 134558667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1326 919 603 41 0 1285 0 vsize: 5304 [startup+130.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 963 0 0 0 12995 3 0 0 25 0 1 0 491687351 5566464 941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1359 941 603 41 0 1318 0 vsize: 5436 [startup+140.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 989 0 0 0 13994 4 0 0 25 0 1 0 491687351 5701632 967 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1392 967 603 41 0 1351 0 vsize: 5568 [startup+150.005 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1034 0 0 0 14994 4 0 0 25 0 1 0 491687351 5836800 1012 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1425 1012 603 41 0 1384 0 vsize: 5700 [startup+160.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1045 0 0 0 15995 4 0 0 25 0 1 0 491687351 5836800 1023 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1425 1023 603 41 0 1384 0 vsize: 5700 [startup+170.004 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1059 0 0 0 16995 4 0 0 25 0 1 0 491687351 5984256 1037 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1461 1037 603 41 0 1420 0 vsize: 5844 [startup+180.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1063 0 0 0 17995 4 0 0 25 0 1 0 491687351 5984256 1041 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1461 1041 603 41 0 1420 0 vsize: 5844 [startup+190.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1102 0 0 0 18995 4 0 0 25 0 1 0 491687351 6115328 1080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1493 1080 603 41 0 1452 0 vsize: 5972 [startup+200.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1105 0 0 0 19995 4 0 0 25 0 1 0 491687351 6115328 1083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1493 1083 603 41 0 1452 0 vsize: 5972 [startup+210.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1125 0 0 0 20995 4 0 0 25 0 1 0 491687351 6250496 1103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1526 1103 603 41 0 1485 0 vsize: 6104 [startup+218.63 s] Raw data (loadavg): 0.99 0.96 0.91 1/53 24699 Raw data (stat): 24699 (minisat+) R 24698 10720 10719 0 -1 0 1125 0 0 0 20995 4 0 0 25 0 1 0 491687351 6250496 1103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1526 1103 603 41 0 1485 0 vsize: 0 Child status: 30 Real time (s): 218.629 CPU time (s): 218.627 CPU user time (s): 218.577 CPU system time (s): 0.049992 CPU usage (%): 99.9988 Max. virtual memory (Kb): 6104 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 788263 #### END VERIFIER DATA ####