Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32b1.opb |
MD5SUM | c4653389ddee2820797c664a0856c651 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 191 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 456 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 456 |
Number of bits of the sum of numbers in the objective function | 9 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 456 |
Number of bits of the biggest sum of numbers | 9 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02784 |
Number of variables | 456 |
Total number of constraints | 1602 |
Number of constraints which are clauses | 1602 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 32 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc8 THE 2005-04-14 03:56:26 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4659 boxname=wulflinc8 idbench=147 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c4653389ddee2820797c664a0856c651 /oldhome/oroussel/tmp/wulflinc8/normalized-ii32b1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-ii32b1.opb /oldhome/oroussel/tmp/wulflinc8/normalized-ii32b1.opb IDLAUNCH: 4659 /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: 875752 kB Buffers: 37692 kB Cached: 99804 kB SwapCached: 0 kB Active: 76724 kB Inactive: 65436 kB HighTotal: 131008 kB HighFree: 25508 kB LowTotal: 903652 kB LowFree: 850244 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6932 kB Slab: 11168 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:59:14 (client local time) WITH STATUS 30 IN 167.602 SECONDS stats: 4659 0 167.602 30 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1602 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1602 6636 | 534 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 216[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:17164 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34 | 42477 102298 | 14159 34 1715 50.4 | 0.000 % | c ============================================================================== c [1mFound solution: 215[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54 | 42515 102409 | 14171 53 2398 45.2 | 0.000 % | c | 154 | 42458 102281 | 15588 152 7262 47.8 | 0.236 % | c | 307 | 42188 101675 | 17146 299 22879 76.5 | 0.751 % | c ============================================================================== c [1mFound solution: 214[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 396 | 41528 100175 | 13842 378 26031 68.9 | 0.751 % | c ============================================================================== c [1mFound solution: 213[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 424 | 41539 100230 | 13846 405 27166 67.1 | 0.751 % | c ============================================================================== c [1mFound solution: 212[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 425 | 41495 100122 | 13831 405 27104 66.9 | 0.751 % | c ============================================================================== c [1mFound solution: 211[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 425 | 41563 100299 | 13854 405 27104 66.9 | 0.751 % | c ============================================================================== c [1mFound solution: 210[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 425 | 41510 100170 | 13836 401 26759 66.7 | 0.751 % | c ============================================================================== c [1mFound solution: 209[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 425 | 41598 100399 | 13866 401 26759 66.7 | 0.751 % | c | 525 | 41598 100399 | 15252 501 30765 61.4 | 2.399 % | c | 675 | 41598 100399 | 16777 651 45675 70.2 | 2.399 % | c ============================================================================== c [1mFound solution: 208[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 719 | 41427 99999 | 13809 687 47468 69.1 | 2.399 % | c | 819 | 39167 94828 | 15189 742 47637 64.2 | 7.581 % | c | 972 | 38485 93263 | 16708 881 57985 65.8 | 9.069 % | c ============================================================================== c [1mFound solution: 207[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1052 | 38552 93437 | 12850 961 62711 65.3 | 9.069 % | c | 1154 | 38552 93437 | 14135 1063 66641 62.7 | 9.064 % | c | 1308 | 38388 93061 | 15548 1213 72567 59.8 | 9.420 % | c | 1534 | 38129 92472 | 17103 1435 82837 57.7 | 9.946 % | c | 1872 | 38052 92295 | 18813 1772 97378 55.0 | 10.117 % | c ============================================================================== c [1mFound solution: 206[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2047 | 37998 92158 | 12666 1944 106801 54.9 | 10.117 % | c | 2149 | 37919 91977 | 13932 2045 111102 54.3 | 10.378 % | c | 2301 | 37838 91791 | 15325 2196 119809 54.6 | 10.556 % | c | 2526 | 37838 91791 | 16858 2421 134310 55.5 | 10.556 % | c | 2863 | 37682 91433 | 18544 2756 160715 58.3 | 10.897 % | c | 3370 | 37544 91119 | 20398 3261 191745 58.8 | 11.181 % | c | 4129 | 37374 90731 | 22438 4018 248749 61.9 | 11.537 % | c ============================================================================== c [1mFound solution: 205[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4525 | 37370 90747 | 12456 4413 278516 63.1 | 11.537 % | c | 4626 | 37370 90747 | 13701 4514 285947 63.3 | 11.698 % | c | 4776 | 33171 81106 | 15071 4537 285171 62.9 | 20.848 % | c | 5002 | 30431 74784 | 16578 4710 295796 62.8 | 27.023 % | c | 5343 | 30130 74089 | 18236 5045 330332 65.5 | 27.704 % | c | 5851 | 30130 74089 | 20060 5553 354344 63.8 | 27.704 % | c | 6610 | 30053 73911 | 22066 6311 408910 64.8 | 27.882 % | c | 7749 | 29958 73694 | 24273 7449 506695 68.0 | 28.081 % | c ============================================================================== c [1mFound solution: 204[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8847 | 29496 72623 | 9832 8522 595069 69.8 | 28.081 % | c | 8947 | 29496 72623 | 10815 8622 600834 69.7 | 29.063 % | c | 9097 | 29496 72623 | 11896 8772 610601 69.6 | 29.063 % | c ============================================================================== c [1mFound solution: 203[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9127 | 29552 72767 | 9850 8802 612351 69.6 | 29.063 % | c | 9229 | 29305 72196 | 10835 8899 617554 69.4 | 29.609 % | c | 9379 | 29305 72196 | 11918 9049 629505 69.6 | 29.609 % | c | 9604 | 29305 72196 | 13110 9274 649848 70.1 | 29.609 % | c | 9943 | 28850 71153 | 14421 9605 677210 70.5 | 30.588 % | c ============================================================================== c [1mFound solution: 202[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9997 | 28802 71031 | 9600 9628 677995 70.4 | 30.588 % | c ============================================================================== c [1mFound solution: 201[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10011 | 28867 71198 | 9622 9642 678740 70.4 | 30.588 % | c ============================================================================== c [1mFound solution: 200[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10026 | 28821 71076 | 9607 9570 667660 69.8 | 30.588 % | c | 10128 | 28758 70932 | 10567 9667 671889 69.5 | 30.878 % | c | 10283 | 28400 70109 | 11624 9638 669626 69.5 | 31.677 % | c | 10511 | 28323 69933 | 12786 9864 682298 69.2 | 31.840 % | c | 10849 | 28234 69728 | 14065 10201 696851 68.3 | 32.038 % | c | 11356 | 28234 69728 | 15472 10708 724790 67.7 | 32.038 % | c | 12116 | 28054 69314 | 17019 11466 772328 67.4 | 32.435 % | c ============================================================================== c [1mFound solution: 199[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12727 | 28110 69458 | 9370 12077 809031 67.0 | 32.435 % | c ============================================================================== c [1mFound solution: 197[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12788 | 28174 69622 | 9391 12138 811923 66.9 | 32.435 % | c | 12888 | 28017 69261 | 10330 12236 815903 66.7 | 32.717 % | c | 13038 | 27669 68465 | 11363 12375 822068 66.4 | 33.451 % | c | 13263 | 27430 67917 | 12499 12597 833838 66.2 | 33.966 % | c | 13600 | 26946 66802 | 13749 12926 847487 65.6 | 35.047 % | c | 14106 | 26946 66802 | 15124 13432 876209 65.2 | 35.047 % | c | 14865 | 26388 65518 | 16636 14185 925056 65.2 | 36.275 % | c ============================================================================== c [1mFound solution: 196[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15370 | 26072 64774 | 8690 14615 941119 64.4 | 36.275 % | c | 15471 | 25969 64537 | 9559 7408 358717 48.4 | 37.181 % | c | 15621 | 25930 64450 | 10514 7434 359569 48.4 | 37.265 % | c | 15847 | 25930 64450 | 11566 7660 376631 49.2 | 37.265 % | c | 16185 | 25657 63820 | 12723 7995 391009 48.9 | 37.879 % | c | 16691 | 25657 63820 | 13995 8501 412097 48.5 | 37.879 % | c ============================================================================== c [1mFound solution: 195[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17347 | 24810 61886 | 8270 9137 461387 50.5 | 37.879 % | c | 17447 | 24810 61886 | 9097 9237 466441 50.5 | 39.818 % | c | 17599 | 24810 61886 | 10006 9389 476409 50.7 | 39.818 % | c | 17825 | 24713 61662 | 11007 9614 491020 51.1 | 40.037 % | c | 18162 | 24713 61662 | 12108 9951 508921 51.1 | 40.037 % | c | 18672 | 24519 61207 | 13318 10459 536023 51.2 | 40.467 % | c | 19431 | 24311 60721 | 14650 11216 575218 51.3 | 40.918 % | c | 20570 | 24007 60007 | 16115 12351 649239 52.6 | 41.603 % | c ============================================================================== c [1mFound solution: 194[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21727 | 23743 59377 | 7914 13365 705426 52.8 | 41.603 % | c | 21828 | 23529 58877 | 8705 13464 707593 52.6 | 42.619 % | c | 21980 | 23529 58877 | 9575 13616 715751 52.6 | 42.618 % | c | 22205 | 23529 58877 | 10533 13841 728136 52.6 | 42.618 % | c ============================================================================== c [1mFound solution: 193[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22250 | 23590 59032 | 7863 13886 731868 52.7 | 42.618 % | c | 22350 | 23590 59032 | 8649 13986 738078 52.8 | 42.571 % | c | 22500 | 23590 59032 | 9514 14136 751044 53.1 | 42.571 % | c | 22726 | 23590 59032 | 10465 14362 765869 53.3 | 42.571 % | c ============================================================================== c [1mFound solution: 192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22997 | 23546 58914 | 7848 14473 761273 52.6 | 42.571 % | c | 23097 | 23546 58914 | 8632 7337 326792 44.5 | 42.664 % | c | 23248 | 23546 58914 | 9496 7488 333622 44.6 | 42.664 % | c | 23474 | 23450 58687 | 10445 7713 344238 44.6 | 42.889 % | c | 23813 | 23251 58218 | 11490 8050 360642 44.8 | 43.347 % | c | 24319 | 23166 58022 | 12639 8554 381315 44.6 | 43.537 % | c | 25079 | 23049 57751 | 13903 9313 425267 45.7 | 43.783 % | c | 26220 | 23049 57751 | 15293 10454 485652 46.5 | 43.784 % | c ============================================================================== c [1mFound solution: 191[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27492 | 22826 57249 | 7608 11718 541938 46.2 | 43.784 % | c | 27593 | 22826 57249 | 8368 11819 546078 46.2 | 44.339 % | c | 27745 | 22826 57249 | 9205 11971 552427 46.1 | 44.340 % | c | 27972 | 22826 57249 | 10126 12198 561303 46.0 | 44.339 % | c | 28310 | 22624 56784 | 11138 12534 581158 46.4 | 44.768 % | c | 28817 | 22624 56784 | 12252 13041 604848 46.4 | 44.769 % | c | 29576 | 22401 56268 | 13478 13798 644548 46.7 | 45.260 % | c | 30715 | 21872 55038 | 14825 14932 689015 46.1 | 46.456 % | c | 32424 | 21468 54093 | 16308 16637 757279 45.5 | 47.405 % | c | 34987 | 21259 53606 | 17939 19198 848234 44.2 | 47.883 % | c | 38832 | 19346 49143 | 19733 22997 995999 43.3 | 52.335 % | c | 44600 | 18591 47383 | 21706 14604 463399 31.7 | 54.065 % | c ============================================================================== c [1mOptimal solution: 191[0m s OPTIMUM FOUND v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 x23 -x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 x55 -x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 x71 -x72 -x73 x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 -x91 x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 -x101 x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 x111 -x112 x113 -x114 x115 -x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 x127 -x128 -x129 -x130 x131 -x132 -x133 x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 -x147 -x148 x149 -x150 x151 -x152 x153 -x154 -x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 -x167 x168 x169 -x170 x171 -x172 x173 -x174 -x175 -x176 -x177 -x178 x179 -x180 x181 -x182 -x183 -x184 -x185 -x186 x187 -x188 x189 -x190 -x191 -x192 -x193 -x194 x195 -x196 -x197 -x198 x199 -x200 x201 -x202 -x203 x204 x205 -x206 x207 -x208 x209 -x210 -x211 -x212 x213 -x214 x215 -x216 x217 -x218 -x219 -x220 -x221 -x222 x223 -x224 x225 -x226 x227 -x228 -x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 -x239 -x240 x241 -x242 -x243 -x244 x245 -x246 -x247 -x248 x249 -x250 x251 -x252 -x253 -x254 x255 -x256 x257 -x258 -x259 -x260 -x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 -x271 x272 x273 -x274 -x275 -x276 x277 -x278 x279 -x280 -x281 -x282 x283 -x284 x285 -x286 x287 -x288 -x289 -x290 x291 -x292 -x293 -x294 x295 -x296 -x297 -x298 x299 -x300 x301 -x302 x303 -x304 x305 -x306 -x307 -x308 -x309 -x310 x311 -x312 x313 -x314 x315 -x316 -x317 -x318 x319 -x320 x321 -x322 -x323 -x324 -x325 -x326 x327 -x328 x329 -x330 x331 -x332 x333 -x334 -x335 -x336 x337 -x338 -x339 -x340 -x341 -x342 x343 -x344 x345 -x346 x347 -x348 x349 -x350 x351 -x352 x353 -x354 x355 -x356 x357 -x358 -x359 -x360 x361 -x362 x363 -x364 -x365 -x366 x367 -x368 x369 -x370 x371 -x372 -x373 -x374 x375 -x376 -x377 x378 x379 -x380 -x381 -x382 x383 -x384 -x385 x386 -x387 x388 x389 -x390 x391 -x392 -x393 x394 -x395 x396 x397 -x398 -x399 x400 -x401 x402 x403 -x404 -x405 x406 -x407 x408 x409 -x410 -x411 x412 -x413 x414 -x415 x416 x417 -x418 -x419 x420 x421 -x422 -x423 x424 -x425 x426 x427 -x428 -x429 x430 -x431 x432 x433 -x434 -x435 x436 -x437 x438 -x439 x440 -x441 x442 x443 -x444 -x445 x446 x447 -x448 -x449 x450 x451 -x452 -x453 x454 -x455 x456 c _______________________________________________________________________________ c c restarts : 103 c conflicts : 48548 (290 /sec) c decisions : 102565 (613 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 167.445 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.86 0.94 0.90 2/54 1454 Raw data (stat): 1454 (runsolver) R 1453 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 409734506 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0009 s] Raw data (loadavg): 0.88 0.94 0.90 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 1775 0 0 0 994 4 0 0 25 0 1 0 409734506 9109504 1737 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2224 1737 603 41 0 2183 0 vsize: 8896 [startup+20.0016 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2028 0 0 0 1992 6 0 0 25 0 1 0 409734506 10182656 1990 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2486 1990 603 41 0 2445 0 vsize: 9944 [startup+30.0019 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2335 0 0 0 2991 7 0 0 25 0 1 0 409734506 11513856 2297 4294967295 134512640 134672761 3221224576 3221222928 134522981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2811 2297 603 41 0 2770 0 vsize: 11244 [startup+40.0022 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2509 0 0 0 3990 8 0 0 25 0 1 0 409734506 12156928 2471 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2968 2471 603 41 0 2927 0 vsize: 11872 [startup+50.003 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2673 0 0 0 4989 9 0 0 25 0 1 0 409734506 12828672 2635 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2635 603 41 0 3091 0 vsize: 12528 [startup+60.0033 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2673 0 0 0 5988 9 0 0 25 0 1 0 409734506 12828672 2635 4294967295 134512640 134672761 3221224576 3221223744 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2635 603 41 0 3091 0 vsize: 12528 [startup+70.0045 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2673 0 0 0 6988 10 0 0 25 0 1 0 409734506 12828672 2635 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2635 603 41 0 3091 0 vsize: 12528 [startup+80.0053 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2673 0 0 0 7988 10 0 0 25 0 1 0 409734506 12828672 2635 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2635 603 41 0 3091 0 vsize: 12528 [startup+90.0057 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2673 0 0 0 8987 11 0 0 25 0 1 0 409734506 12828672 2635 4294967295 134512640 134672761 3221224576 3221223680 134560352 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2635 603 41 0 3091 0 vsize: 12528 [startup+100.006 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2676 0 0 0 9987 11 0 0 25 0 1 0 409734506 12828672 2638 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3132 2638 603 41 0 3091 0 vsize: 12528 [startup+110.007 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2701 0 0 0 10986 11 0 0 25 0 1 0 409734506 12972032 2663 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3167 2663 603 41 0 3126 0 vsize: 12668 [startup+120.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2708 0 0 0 11986 12 0 0 25 0 1 0 409734506 13103104 2670 4294967295 134512640 134672761 3221224576 3221223760 134559365 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3199 2670 603 41 0 3158 0 vsize: 12796 [startup+130.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2811 0 0 0 12986 12 0 0 25 0 1 0 409734506 13508608 2773 4294967295 134512640 134672761 3221224576 3221223744 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3298 2773 603 41 0 3257 0 vsize: 13192 [startup+140.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 2909 0 0 0 13985 13 0 0 25 0 1 0 409734506 13901824 2871 4294967295 134512640 134672761 3221224576 3221223720 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3394 2871 603 41 0 3353 0 vsize: 13576 [startup+150.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 3007 0 0 0 14984 13 0 0 25 0 1 0 409734506 14299136 2969 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3491 2969 603 41 0 3450 0 vsize: 13964 [startup+160.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 3031 0 0 0 15984 14 0 0 25 0 1 0 409734506 14299136 2993 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3491 2993 603 41 0 3450 0 vsize: 13964 [startup+167.629 s] Raw data (loadavg): 0.99 0.96 0.91 1/53 1454 Raw data (stat): 1454 (minisat+) R 1453 26667 26666 0 -1 0 3031 0 0 0 15984 14 0 0 25 0 1 0 409734506 14299136 2993 4294967295 134512640 134672761 3221224576 3221223744 134561027 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3491 2993 603 41 0 3450 0 vsize: 0 Child status: 30 Real time (s): 167.629 CPU time (s): 167.602 CPU user time (s): 167.449 CPU system time (s): 0.152976 CPU usage (%): 99.9837 Max. virtual memory (Kb): 13964 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: OK 191 #### END VERIFIER DATA ####