Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb |
MD5SUM | c2339539ffa69702e62053614fe34ce1 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 44800 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 252 |
Biggest coefficient in the objective function | 2621440 |
Number of bits for the biggest coefficient in the objective function | 22 |
Sum of the numbers in the objective function | 35682270 |
Number of bits of the sum of numbers in the objective function | 26 |
Biggest number in a constraint | 2621440 |
Number of bits of the biggest number in a constraint | 22 |
Biggest sum of numbers in a constraint | 35682270 |
Number of bits of the biggest sum of numbers | 26 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 24.1133 |
Number of variables | 252 |
Total number of constraints | 19 |
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 | 19 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc27 THE 2005-04-21 12:24:05 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18977 boxname=wulflinc27 idbench=1460 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c2339539ffa69702e62053614fe34ce1 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bk4x3.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bk4x3.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-bk4x3.opb IDLAUNCH: 18977 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 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 : 3 cpu MHz : 451.169 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: 754256 kB Buffers: 21892 kB Cached: 233956 kB SwapCached: 512 kB Active: 14564 kB Inactive: 243220 kB HighTotal: 131008 kB HighFree: 46228 kB LowTotal: 903652 kB LowFree: 708028 kB SwapTotal: 2097892 kB SwapFree: 2096480 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5104 kB Slab: 16880 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 12:24:40 (client local time) WITH STATUS 30 IN 35.5136 SECONDS stats: 18977 0 35.5136 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 26 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 24]---> Adder-cost: 44 maxlim: 4861 bits: 13/13 c ---[ 22]---> Adder-cost: 48 maxlim: 8445 bits: 14/14 c ---[ 20]---> Adder-cost: 48 maxlim: 11261 bits: 14/14 c ---[ 18]---> Adder-cost: 48 maxlim: 9725 bits: 14/14 c ---[ 16]---> Adder-cost: 72 maxlim: 11772 bits: 14/14 c ---[ 14]---> Adder-cost: 76 maxlim: 12028 bits: 15/14 c ---[ 12]---> Adder-cost: 72 maxlim: 10492 bits: 14/14 c ---[ 11]---> Adder-cost: 6 maxlim: 2046 bits: 12/11 c ---[ 10]---> Adder-cost: 6 maxlim: 2046 bits: 12/11 c ---[ 9]---> Adder-cost: 6 maxlim: 4094 bits: 13/12 c ---[ 8]---> Adder-cost: 6 maxlim: 4094 bits: 13/12 c ---[ 7]---> Adder-cost: 6 maxlim: 2046 bits: 12/11 c ---[ 6]---> Adder-cost: 6 maxlim: 4094 bits: 13/12 c ---[ 5]---> Adder-cost: 8 maxlim: 4094 bits: 13/12 c ---[ 4]---> Adder-cost: 8 maxlim: 4094 bits: 13/12 c ---[ 3]---> Adder-cost: 6 maxlim: 4094 bits: 13/12 c ---[ 2]---> Adder-cost: 6 maxlim: 8190 bits: 14/13 c ---[ 1]---> Adder-cost: 8 maxlim: 4094 bits: 13/12 c ---[ 0]---> Adder-cost: 6 maxlim: 4094 bits: 13/12 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 2863 10630 | 954 0 0 nan | 0.000 % | c | 100 | 2863 10630 | 1049 100 862 8.6 | 44.799 % | c | 250 | 2863 10630 | 1154 250 1566 6.3 | 44.799 % | c | 475 | 2863 10630 | 1269 475 3235 6.8 | 44.799 % | c ============================================================================== c [1mFound solution: 66846[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 400 maxlim: 101056 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 576 | 5593 20384 | 1864 576 3946 6.9 | 44.799 % | c ============================================================================== c [1mFound solution: 63614[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 104288 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 591 | 5613 20513 | 1871 591 4029 6.8 | 44.799 % | c | 691 | 5613 20513 | 2058 691 4573 6.6 | 32.395 % | c | 841 | 5613 20513 | 2263 841 9060 10.8 | 32.395 % | c | 1067 | 5613 20513 | 2490 1067 15335 14.4 | 32.395 % | c ============================================================================== c [1mFound solution: 61952[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 105950 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1128 | 5639 20715 | 1879 1128 16283 14.4 | 32.395 % | c ============================================================================== c [1mFound solution: 56320[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 111582 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1133 | 5658 20877 | 1886 1133 16300 14.4 | 32.395 % | c ============================================================================== c [1mFound solution: 53760[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 114142 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1133 | 5677 21007 | 1892 1133 16300 14.4 | 32.395 % | c ============================================================================== c [1mFound solution: 52480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 115422 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1133 | 5696 21154 | 1898 1133 16300 14.4 | 32.395 % | c ============================================================================== c [1mFound solution: 49920[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 117982 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1137 | 5712 21275 | 1904 1137 16513 14.5 | 32.395 % | c | 1238 | 5712 21275 | 2094 1238 17889 14.4 | 33.995 % | c | 1388 | 5712 21275 | 2303 1388 21497 15.5 | 33.993 % | c | 1614 | 5712 21275 | 2534 1614 26349 16.3 | 33.993 % | c | 1952 | 5712 21275 | 2787 1952 34256 17.5 | 33.993 % | c | 2459 | 5712 21275 | 3066 2459 45862 18.7 | 33.993 % | c | 3219 | 5712 21275 | 3373 3219 62891 19.5 | 33.993 % | c | 4360 | 5712 21275 | 3710 2374 41050 17.3 | 33.993 % | c ============================================================================== c [1mFound solution: 48516[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 119386 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5666 | 5722 21378 | 1907 3680 76694 20.8 | 33.993 % | c | 5766 | 5722 21378 | 2097 1940 33486 17.3 | 34.237 % | c | 5916 | 5722 21378 | 2307 2090 37611 18.0 | 34.237 % | c | 6142 | 5722 21378 | 2538 2316 42044 18.2 | 34.237 % | c | 6485 | 5707 21331 | 2792 2658 50204 18.9 | 34.441 % | c | 6991 | 5707 21331 | 3071 3164 61324 19.4 | 34.441 % | c | 7751 | 5707 21331 | 3378 2107 30926 14.7 | 34.441 % | c | 8890 | 5707 21331 | 3716 3246 53804 16.6 | 34.441 % | c | 10601 | 5707 21331 | 4087 2792 42495 15.2 | 34.441 % | c | 13163 | 5707 21331 | 4496 3018 43939 14.6 | 34.441 % | c ============================================================================== c [1mFound solution: 48388[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 119514 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14109 | 5719 21424 | 1906 3964 64677 16.3 | 34.441 % | c | 14209 | 5719 21424 | 2096 2082 26770 12.9 | 34.566 % | c | 14359 | 5719 21424 | 2306 2232 30106 13.5 | 34.566 % | c | 14585 | 5719 21424 | 2536 2458 34111 13.9 | 34.566 % | c | 14922 | 5719 21424 | 2790 2795 42037 15.0 | 34.566 % | c | 15428 | 5719 21424 | 3069 3301 54225 16.4 | 34.566 % | c | 16187 | 5719 21424 | 3376 2223 34387 15.5 | 34.566 % | c | 17327 | 5719 21424 | 3714 3363 76445 22.7 | 34.566 % | c | 19035 | 5719 21424 | 4085 2924 46486 15.9 | 34.566 % | c | 21598 | 5719 21424 | 4494 3134 51177 16.3 | 34.566 % | c ============================================================================== c [1mFound solution: 47872[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 120030 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23818 | 5735 21533 | 1911 2823 51850 18.4 | 34.566 % | c | 23919 | 5735 21533 | 2102 1513 21352 14.1 | 34.731 % | c | 24069 | 5735 21533 | 2312 1663 24524 14.7 | 34.731 % | c | 24295 | 5718 21482 | 2543 1887 28589 15.2 | 34.997 % | c | 24633 | 5718 21482 | 2797 2225 41489 18.6 | 34.997 % | c | 25139 | 5718 21482 | 3077 2731 55793 20.4 | 34.997 % | c ============================================================================== c [1mFound solution: 47360[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 120542 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 25640 | 5734 21592 | 1911 3232 70528 21.8 | 34.997 % | c | 25742 | 5734 21592 | 2102 1718 24786 14.4 | 35.155 % | c | 25893 | 5734 21592 | 2312 1869 28719 15.4 | 35.155 % | c | 26118 | 5734 21592 | 2543 2094 34526 16.5 | 35.155 % | c | 26455 | 5734 21592 | 2797 2431 42123 17.3 | 35.155 % | c | 26965 | 5734 21592 | 3077 2941 54569 18.6 | 35.155 % | c | 27726 | 5734 21592 | 3385 3702 75075 20.3 | 35.155 % | c | 28865 | 5734 21592 | 3723 2832 50042 17.7 | 35.155 % | c | 30573 | 5734 21592 | 4096 2366 37165 15.7 | 35.155 % | c | 33135 | 5734 21592 | 4506 2548 49134 19.3 | 35.155 % | c ============================================================================== c [1mFound solution: 47104[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 120798 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33182 | 5750 21703 | 1916 2595 50437 19.4 | 35.155 % | c | 33285 | 5750 21703 | 2107 1401 14249 10.2 | 35.309 % | c | 33437 | 5750 21703 | 2318 1553 17669 11.4 | 35.309 % | c | 33663 | 5750 21703 | 2550 1779 22481 12.6 | 35.310 % | c | 34001 | 5750 21703 | 2805 2117 29157 13.8 | 35.309 % | c | 34508 | 5750 21703 | 3085 2624 41243 15.7 | 35.309 % | c | 35267 | 5750 21703 | 3394 3383 61752 18.3 | 35.309 % | c ============================================================================== c [1mFound solution: 46080[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 121822 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36009 | 5770 21829 | 1923 2084 31251 15.0 | 35.309 % | c | 36109 | 5770 21829 | 2115 2184 33784 15.5 | 35.498 % | c | 36259 | 5770 21829 | 2326 2334 37263 16.0 | 35.498 % | c | 36485 | 5770 21829 | 2559 2560 43118 16.8 | 35.498 % | c | 36822 | 5770 21829 | 2815 2897 49280 17.0 | 35.498 % | c | 37330 | 5770 21829 | 3097 3405 61610 18.1 | 35.498 % | c | 38090 | 5770 21829 | 3406 2282 33458 14.7 | 35.498 % | c | 39230 | 5770 21829 | 3747 3422 56072 16.4 | 35.498 % | c | 40940 | 5770 21829 | 4122 2954 44531 15.1 | 35.498 % | c ============================================================================== c [1mFound solution: 44800[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 123102 bits: 18/17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 42158 | 5785 21933 | 1928 4172 72123 17.3 | 35.498 % | c | 42259 | 5785 21933 | 2120 2187 29936 13.7 | 35.669 % | c | 42411 | 5785 21933 | 2332 2339 33112 14.2 | 35.669 % | c | 42636 | 5785 21933 | 2566 2564 37365 14.6 | 35.669 % | c | 42973 | 5785 21933 | 2822 2901 44721 15.4 | 35.669 % | c | 43481 | 5785 21933 | 3105 3409 56349 16.5 | 35.669 % | c | 44241 | 5785 21933 | 3415 2296 33105 14.4 | 35.669 % | c | 45380 | 5785 21933 | 3757 3435 54748 15.9 | 35.669 % | c | 47088 | 5785 21933 | 4132 2959 43027 14.5 | 35.669 % | c | 49652 | 5785 21933 | 4546 3162 45839 14.5 | 35.669 % | c | 53497 | 5785 21933 | 5000 4420 75702 17.1 | 35.669 % | c | 59264 | 5785 21933 | 5500 4546 68270 15.0 | 35.669 % | c | 67913 | 5779 21916 | 6050 4037 57893 14.3 | 35.733 % | c | 80887 | 5779 21916 | 6655 3682 47926 13.0 | 35.733 % | c | 100348 | 5772 21893 | 7321 4965 61823 12.5 | 35.797 % | c ============================================================================== c [1mOptimal solution: 44800[0m s OPTIMUM FOUND v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0 c _______________________________________________________________________________ c c restarts : 88 c conflicts : 106328 (2997 /sec) c decisions : 139591 (3934 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 35.4796 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.91 0.95 0.91 2/54 19417 Raw data (stat): 19417 (runsolver) R 19416 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545052094 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+10.0003 s] Raw data (loadavg): 0.93 0.95 0.91 2/54 19417 Raw data (stat): 19417 (minisat+) R 19416 18865 18864 0 -1 0 643 0 0 0 996 2 0 0 25 0 1 0 545052094 4169728 621 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1018 621 603 41 0 977 0 vsize: 4072 [startup+20.0014 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 19417 Raw data (stat): 19417 (minisat+) R 19416 18865 18864 0 -1 0 703 0 0 0 1996 2 0 0 25 0 1 0 545052094 4440064 681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1084 681 603 41 0 1043 0 vsize: 4336 [startup+30.001 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 19417 Raw data (stat): 19417 (minisat+) R 19416 18865 18864 0 -1 0 743 0 0 0 2995 3 0 0 25 0 1 0 545052094 4575232 721 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1117 721 603 41 0 1076 0 vsize: 4468 [startup+35.5289 s] Raw data (loadavg): 0.95 0.96 0.91 1/53 19417 Raw data (stat): 19417 (minisat+) R 19416 18865 18864 0 -1 0 743 0 0 0 2995 3 0 0 25 0 1 0 545052094 4575232 721 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1117 721 603 41 0 1076 0 vsize: 0 Child status: 30 Real time (s): 35.5286 CPU time (s): 35.5136 CPU user time (s): 35.4806 CPU system time (s): 0.032994 CPU usage (%): 99.9576 Max. virtual memory (Kb): 4468 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 44800 #### END VERIFIER DATA ####