Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-p0291.opb |
MD5SUM | 1d9168a9335e29df835d07b0bdf2adea |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 10447498 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 289 |
Biggest coefficient in the objective function | 80000000 |
Number of bits for the biggest coefficient in the objective function | 27 |
Sum of the numbers in the objective function | 686518451 |
Number of bits of the sum of numbers in the objective function | 30 |
Biggest number in a constraint | 80000000 |
Number of bits of the biggest number in a constraint | 27 |
Biggest sum of numbers in a constraint | 686518451 |
Number of bits of the biggest sum of numbers | 30 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 0.335948 |
Number of variables | 291 |
Total number of constraints | 543 |
Number of constraints which are clauses | 189 |
Number of constraints which are cardinality constraints (but not clauses) | 295 |
Number of constraints which are nor clauses,nor cardinality constraints | 59 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 53 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc28 THE 2005-04-22 02:01:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12155 boxname=wulflinc28 idbench=935 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1d9168a9335e29df835d07b0bdf2adea /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0291.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0291.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0291.opb IDLAUNCH: 12155 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 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: 306312 kB Buffers: 17440 kB Cached: 686188 kB SwapCached: 104 kB Active: 41960 kB Inactive: 664108 kB HighTotal: 131008 kB HighFree: 30380 kB LowTotal: 903652 kB LowFree: 275932 kB SwapTotal: 2097640 kB SwapFree: 2097068 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6056 kB Slab: 16684 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-22 02:21:59 (client local time) WITH STATUS 10 IN 1200.21 SECONDS stats: 12155 7 1200.21 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 205 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .............................................................................................................................................................................................sssss c ---[ 144]---> BDD-cost: 3 c ---[ 139]---> BDD-cost: 3 c ---[ 14]---> Sorter-cost: 1503 Base: 2 2 5 2 3 c ---[ 13]---> Sorter-cost: 1241 Base: 2 2 5 2 3 c ---[ 11]---> BDD-cost: 52 c ---[ 10]---> BDD-cost: 52 c ---[ 9]---> BDD-cost: 52 c ---[ 8]---> BDD-cost: 12 c ---[ 7]---> BDD-cost: 8 c ---[ 6]---> BDD-cost: 16 c ---[ 5]---> BDD-cost: 28 c ---[ 4]---> BDD-cost: 12 c ---[ 3]---> BDD-cost: 86 c ---[ 2]---> Sorter-cost: 749 Base: 2 5 2 2 c ---[ 1]---> Sorter-cost: 880 Base: 2 2 5 3 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11271 26846 | 3757 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 160963526[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:118482 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8 | 356963 835866 | 118987 7 39 5.6 | 0.000 % | c | 108 | 356956 835851 | 130885 106 2431 22.9 | 0.024 % | c | 258 | 356956 835851 | 143974 256 3715 14.5 | 0.024 % | c | 484 | 356956 835851 | 158371 482 5549 11.5 | 0.024 % | c | 822 | 356956 835851 | 174208 820 8532 10.4 | 0.024 % | c | 1329 | 356941 835818 | 191629 1326 13300 10.0 | 0.027 % | c | 2090 | 356857 835631 | 210792 2083 26782 12.9 | 0.046 % | c | 3231 | 356857 835631 | 231872 3224 82835 25.7 | 0.046 % | c | 4941 | 356552 834948 | 255059 4927 112930 22.9 | 0.113 % | c ============================================================================== c [1mFound solution: 118952803[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 23 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6131 | 358296 839637 | 119432 6113 141375 23.1 | 0.113 % | c | 6231 | 358296 839637 | 131375 6213 142715 23.0 | 0.164 % | c | 6381 | 358296 839637 | 144512 6363 151312 23.8 | 0.164 % | c | 6606 | 358296 839637 | 158963 6588 157024 23.8 | 0.164 % | c ============================================================================== c [1mFound solution: 118814390[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 22 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6662 | 359024 841543 | 119674 6637 159413 24.0 | 0.164 % | c ============================================================================== c [1mFound solution: 114022192[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6743 | 358970 841447 | 119656 6707 161204 24.0 | 0.164 % | c | 6844 | 358963 841432 | 131621 6807 167695 24.6 | 0.242 % | c ============================================================================== c [1mFound solution: 104115770[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6975 | 359177 841952 | 119725 6938 172621 24.9 | 0.242 % | c | 7075 | 359177 841952 | 131697 7038 174869 24.8 | 0.242 % | c | 7225 | 359166 841928 | 144867 7187 176150 24.5 | 0.245 % | c | 7450 | 358833 841174 | 159353 7408 177671 24.0 | 0.320 % | c | 7788 | 358833 841174 | 175289 7746 181482 23.4 | 0.320 % | c | 8297 | 358833 841174 | 192818 8255 197847 24.0 | 0.320 % | c | 9057 | 358833 841174 | 212100 9015 231628 25.7 | 0.320 % | c | 10196 | 358519 840458 | 233310 10150 274795 27.1 | 0.394 % | c ============================================================================== c [1mFound solution: 103894941[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 22 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11225 | 358601 840684 | 119533 11179 316767 28.3 | 0.394 % | c | 11328 | 358601 840684 | 131486 11282 327789 29.1 | 0.394 % | c | 11478 | 358470 840389 | 144634 11429 329959 28.9 | 0.421 % | c | 11703 | 358470 840389 | 159098 11654 346815 29.8 | 0.421 % | c | 12042 | 358423 840284 | 175008 11990 350509 29.2 | 0.431 % | c ============================================================================== c [1mFound solution: 103270240[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12469 | 358614 840779 | 119538 12359 387924 31.4 | 0.431 % | c | 12569 | 358614 840779 | 131491 12459 389236 31.2 | 0.463 % | c | 12720 | 358581 840704 | 144640 12609 390327 31.0 | 0.471 % | c | 12946 | 358581 840704 | 159105 12835 391879 30.5 | 0.471 % | c | 13285 | 358581 840704 | 175015 13174 398984 30.3 | 0.471 % | c | 13791 | 358457 840424 | 192517 13671 405790 29.7 | 0.500 % | c | 14553 | 358418 840336 | 211768 14432 431113 29.9 | 0.509 % | c | 15692 | 358320 840117 | 232945 15567 447980 28.8 | 0.530 % | c ============================================================================== c [1mFound solution: 103270025[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 23 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16574 | 358367 840282 | 119455 16444 463985 28.2 | 0.530 % | c | 16675 | 358367 840282 | 131400 16545 465001 28.1 | 0.548 % | c | 16825 | 358367 840282 | 144540 16695 495310 29.7 | 0.548 % | c | 17050 | 358367 840282 | 158994 16920 498450 29.5 | 0.548 % | c | 17387 | 358089 839656 | 174894 17255 500675 29.0 | 0.609 % | c ============================================================================== c [1mFound solution: 103209779[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 24 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17860 | 358178 839891 | 119392 17728 505821 28.5 | 0.609 % | c | 17960 | 358178 839891 | 131331 17828 506451 28.4 | 0.610 % | c ============================================================================== c [1mFound solution: 102506300[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18073 | 358214 839983 | 119404 17941 508901 28.4 | 0.610 % | c ============================================================================== c [1mFound solution: 102224061[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 17 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18165 | 358260 840097 | 119420 18033 514182 28.5 | 0.610 % | c | 18265 | 358260 840097 | 131362 18133 515968 28.5 | 0.611 % | c | 18415 | 358260 840097 | 144498 18283 526879 28.8 | 0.611 % | c | 18640 | 358032 839582 | 158948 18499 530080 28.7 | 0.663 % | c | 18978 | 357689 838798 | 174842 18830 533078 28.3 | 0.748 % | c | 19485 | 357689 838798 | 192327 19337 543967 28.1 | 0.748 % | c | 20247 | 357579 838546 | 211559 20095 554914 27.6 | 0.775 % | c ============================================================================== c [1mFound solution: 101392970[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20842 | 357166 837606 | 119055 20657 600327 29.1 | 0.775 % | c | 20942 | 357166 837606 | 130960 20757 604926 29.1 | 0.888 % | c | 21092 | 357099 837455 | 144056 20905 605720 29.0 | 0.903 % | c | 21318 | 357099 837455 | 158462 21131 610735 28.9 | 0.903 % | c | 21655 | 357000 837230 | 174308 21459 613269 28.6 | 0.926 % | c | 22163 | 356996 837221 | 191739 21966 625727 28.5 | 0.926 % | c | 22924 | 356996 837221 | 210913 22727 678511 29.9 | 0.926 % | c | 24063 | 356927 837064 | 232004 23856 710613 29.8 | 0.943 % | c | 25772 | 356927 837064 | 255204 25565 837250 32.7 | 0.943 % | c ============================================================================== c [1mFound solution: 101209457[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 24 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26629 | 356906 837027 | 118968 26419 903304 34.2 | 0.943 % | c | 26730 | 356906 837027 | 130864 26520 903891 34.1 | 0.961 % | c | 26880 | 356906 837027 | 143951 26670 904828 33.9 | 0.961 % | c | 27105 | 356906 837027 | 158346 26895 907211 33.7 | 0.961 % | c | 27442 | 356817 836824 | 174181 27226 910172 33.4 | 0.983 % | c ============================================================================== c [1mFound solution: 91878024[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27886 | 356812 836822 | 118937 27668 917057 33.1 | 0.983 % | c | 27988 | 356812 836822 | 130830 27770 917800 33.1 | 0.994 % | c | 28139 | 356765 836716 | 143913 27920 918595 32.9 | 1.005 % | c | 28364 | 356734 836647 | 158305 28142 920650 32.7 | 1.012 % | c | 28702 | 356730 836638 | 174135 28479 931889 32.7 | 1.013 % | c ============================================================================== c [1mFound solution: 81766179[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 17 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29167 | 356674 836522 | 118891 28941 952174 32.9 | 1.013 % | c | 29270 | 356674 836522 | 130780 29044 956347 32.9 | 1.035 % | c | 29420 | 356674 836522 | 143858 29194 959919 32.9 | 1.035 % | c ============================================================================== c [1mFound solution: 81765994[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 29478 | 356706 836606 | 118902 29252 961145 32.9 | 1.035 % | c | 29578 | 356368 835829 | 130792 29333 963197 32.8 | 1.119 % | c | 29728 | 356368 835829 | 143871 29483 970008 32.9 | 1.119 % | c | 29953 | 356368 835829 | 158258 29708 979702 33.0 | 1.119 % | c | 30291 | 356368 835829 | 174084 30046 987186 32.9 | 1.119 % | c ============================================================================== c [1mFound solution: 81765987[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 3 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30782 | 356083 835189 | 118694 30530 1000135 32.8 | 1.119 % | c | 30882 | 356083 835189 | 130563 30630 1006518 32.9 | 1.195 % | c | 31032 | 356083 835189 | 143619 30780 1007510 32.7 | 1.195 % | c | 31257 | 355449 833743 | 157981 30984 1008809 32.6 | 1.336 % | c | 31594 | 355354 833523 | 173779 31312 1022563 32.7 | 1.362 % | c | 32100 | 355227 833233 | 191157 31807 1041189 32.7 | 1.394 % | c ============================================================================== c [1mFound solution: 78048625[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:80414 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32531 | 584812 1371002 | 194937 32196 1048887 32.6 | 1.394 % | c | 32631 | 584812 1371002 | 214430 32296 1052236 32.6 | 1.188 % | c | 32782 | 584371 1370009 | 235873 32357 1045968 32.3 | 1.253 % | c | 33007 | 584371 1370009 | 259461 32582 1047782 32.2 | 1.253 % | c | 33345 | 584371 1370009 | 285407 32920 1052900 32.0 | 1.253 % | c | 33851 | 583844 1368828 | 313947 33418 1063008 31.8 | 1.326 % | c ============================================================================== c [1mFound solution: 78006987[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34192 | 585022 1371938 | 195007 33759 1078902 32.0 | 1.326 % | c | 34292 | 585022 1371938 | 214507 33859 1081517 31.9 | 1.327 % | c ============================================================================== c [1mFound solution: 77996383[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34345 | 585148 1372288 | 195049 33912 1083510 32.0 | 1.327 % | c | 34446 | 585148 1372288 | 214553 34013 1085853 31.9 | 1.328 % | c | 34596 | 585148 1372288 | 236009 34163 1094197 32.0 | 1.328 % | c | 34821 | 585027 1372018 | 259610 34387 1115333 32.4 | 1.345 % | c | 35158 | 585027 1372018 | 285571 34724 1141357 32.9 | 1.345 % | c ============================================================================== c [1mFound solution: 77992506[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 5 2 2 2 2 2 2 2 2 2 3 2 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 35348 | 584533 1370900 | 194844 34869 1148248 32.9 | 1.345 % | c | 35448 | 584533 1370900 | 214328 34969 1148843 32.9 | 1.427 % | c | 35598 | 584533 1370900 | 235761 35119 1150077 32.7 | 1.427 % | c | 35823 | 584488 1370797 | 259337 35335 1152635 32.6 | 1.434 % | c | 36161 | 584046 1369776 | 285271 35642 1161312 32.6 | 1.505 % | c | 36669 | 583746 1369086 | 313798 36143 1164468 32.2 | 1.550 % | c | 37428 | 583242 1367938 | 345178 36890 1187644 32.2 | 1.623 % | c | 38567 | 583242 1367938 | 379695 38029 1271615 33.4 | 1.623 % | #### 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.93 0.99 0.99 1/54 4273 Raw data (stat): 4273 (runsolver) R 4272 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549967576 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.94 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 903 0 0 0 996 1 0 0 25 0 1 0 549967576 4780032 756 4294967295 134512640 134672761 3221224544 3221222240 134597218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1167 756 603 41 0 1126 0 vsize: 4668 [startup+19.9998 s] Raw data (loadavg): 0.95 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 903 0 0 0 1996 1 0 0 25 0 1 0 549967576 4780032 756 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1167 756 603 41 0 1126 0 vsize: 4668 [startup+30.0002 s] Raw data (loadavg): 0.96 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 903 0 0 0 2996 1 0 0 25 0 1 0 549967576 4780032 756 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1167 756 603 41 0 1126 0 vsize: 4668 [startup+40.0003 s] Raw data (loadavg): 0.96 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 903 0 0 0 3996 2 0 0 25 0 1 0 549967576 4780032 756 4294967295 134512640 134672761 3221224544 3221222672 134597218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1167 756 603 41 0 1126 0 vsize: 4668 [startup+50.0009 s] Raw data (loadavg): 0.97 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10129 0 0 0 4972 25 0 0 25 0 1 0 549967576 42811392 9668 4294967295 134512640 134672761 3221224544 3221223680 134565140 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10452 9668 603 41 0 10411 0 vsize: 41808 [startup+60.0015 s] Raw data (loadavg): 0.97 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10239 0 0 0 5972 26 0 0 25 0 1 0 549967576 43220992 9778 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10552 9778 603 41 0 10511 0 vsize: 42208 [startup+70.0013 s] Raw data (loadavg): 0.98 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10669 0 0 0 6970 28 0 0 25 0 1 0 549967576 44384256 10083 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10836 10083 603 41 0 10795 0 vsize: 43344 [startup+80.0019 s] Raw data (loadavg): 0.98 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10669 0 0 0 7970 28 0 0 25 0 1 0 549967576 44384256 10083 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10836 10083 603 41 0 10795 0 vsize: 43344 [startup+90.0016 s] Raw data (loadavg): 0.98 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10669 0 0 0 8970 28 0 0 25 0 1 0 549967576 44384256 10083 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10836 10083 603 41 0 10795 0 vsize: 43344 [startup+100.002 s] Raw data (loadavg): 0.98 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10669 0 0 0 9971 28 0 0 25 0 1 0 549967576 44384256 10083 4294967295 134512640 134672761 3221224544 3221222960 134597191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10836 10083 603 41 0 10795 0 vsize: 43344 [startup+110.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10669 0 0 0 10971 28 0 0 25 0 1 0 549967576 44384256 10083 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10836 10083 603 41 0 10795 0 vsize: 43344 [startup+120.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10846 0 0 0 11970 28 0 0 25 0 1 0 549967576 44638208 10131 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10131 603 41 0 10857 0 vsize: 43592 [startup+130.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10846 0 0 0 12970 28 0 0 25 0 1 0 549967576 44638208 10131 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10131 603 41 0 10857 0 vsize: 43592 [startup+140.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10846 0 0 0 13970 28 0 0 25 0 1 0 549967576 44638208 10131 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10131 603 41 0 10857 0 vsize: 43592 [startup+150.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10846 0 0 0 14971 28 0 0 25 0 1 0 549967576 44638208 10131 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10131 603 41 0 10857 0 vsize: 43592 [startup+160.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10846 0 0 0 15971 28 0 0 25 0 1 0 549967576 44638208 10131 4294967295 134512640 134672761 3221224544 3221222500 1075351040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10131 603 41 0 10857 0 vsize: 43592 [startup+170.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10986 0 0 0 16970 29 0 0 25 0 1 0 549967576 44638208 10146 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10146 603 41 0 10857 0 vsize: 43592 [startup+180.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10986 0 0 0 17971 29 0 0 25 0 1 0 549967576 44638208 10146 4294967295 134512640 134672761 3221224544 3221221664 134597191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10146 603 41 0 10857 0 vsize: 43592 [startup+190.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10986 0 0 0 18971 29 0 0 25 0 1 0 549967576 44638208 10146 4294967295 134512640 134672761 3221224544 3221221952 134597193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10146 603 41 0 10857 0 vsize: 43592 [startup+200.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 10986 0 0 0 19971 29 0 0 25 0 1 0 549967576 44638208 10146 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10898 10146 603 41 0 10857 0 vsize: 43592 [startup+210.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11030 0 0 0 20971 29 0 0 25 0 1 0 549967576 44810240 10190 4294967295 134512640 134672761 3221224544 3221197024 134594086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10940 10190 603 41 0 10899 0 vsize: 43760 [startup+220.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11136 0 0 0 21971 29 0 0 25 0 1 0 549967576 44666880 10168 4294967295 134512640 134672761 3221224544 3221222208 134522369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10905 10168 603 41 0 10864 0 vsize: 43620 [startup+230.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11136 0 0 0 22971 29 0 0 25 0 1 0 549967576 44666880 10168 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10905 10168 603 41 0 10864 0 vsize: 43620 [startup+240.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11136 0 0 0 23971 29 0 0 25 0 1 0 549967576 44666880 10168 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10905 10168 603 41 0 10864 0 vsize: 43620 [startup+250.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4273 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11136 0 0 0 24972 29 0 0 25 0 1 0 549967576 44666880 10168 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10905 10168 603 41 0 10864 0 vsize: 43620 [startup+260.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11137 0 0 0 25972 29 0 0 25 0 1 0 549967576 44666880 10169 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10905 10169 603 41 0 10864 0 vsize: 43620 [startup+270.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11178 0 0 0 26971 29 0 0 25 0 1 0 549967576 44937216 10210 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10971 10210 603 41 0 10930 0 vsize: 43884 [startup+280.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11216 0 0 0 27971 30 0 0 25 0 1 0 549967576 45072384 10248 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11004 10248 603 41 0 10963 0 vsize: 44016 [startup+290.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11429 0 0 0 28971 30 0 0 25 0 1 0 549967576 45121536 10280 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11016 10280 603 41 0 10975 0 vsize: 44064 [startup+300.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11429 0 0 0 29972 30 0 0 25 0 1 0 549967576 45121536 10280 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11016 10280 603 41 0 10975 0 vsize: 44064 [startup+310.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11429 0 0 0 30972 30 0 0 25 0 1 0 549967576 45121536 10280 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11016 10280 603 41 0 10975 0 vsize: 44064 [startup+320.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11429 0 0 0 31972 30 0 0 25 0 1 0 549967576 45121536 10280 4294967295 134512640 134672761 3221224544 3221222928 134522369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11016 10280 603 41 0 10975 0 vsize: 44064 [startup+330.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11446 0 0 0 32972 30 0 0 25 0 1 0 549967576 45256704 10293 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11049 10293 603 41 0 11008 0 vsize: 44196 [startup+340.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11704 0 0 0 33971 31 0 0 25 0 1 0 549967576 45477888 10368 4294967295 134512640 134672761 3221224544 3221221520 134597269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11103 10368 603 41 0 11062 0 vsize: 44412 [startup+350.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11704 0 0 0 34971 31 0 0 25 0 1 0 549967576 45477888 10368 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11103 10368 603 41 0 11062 0 vsize: 44412 [startup+360.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11704 0 0 0 35971 31 0 0 25 0 1 0 549967576 45477888 10368 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11103 10368 603 41 0 11062 0 vsize: 44412 [startup+370.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11704 0 0 0 36971 31 0 0 25 0 1 0 549967576 45477888 10368 4294967295 134512640 134672761 3221224544 3221222528 134597195 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11103 10368 603 41 0 11062 0 vsize: 44412 [startup+380.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11705 0 0 0 37972 31 0 0 25 0 1 0 549967576 45477888 10368 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11103 10368 603 41 0 11062 0 vsize: 44412 [startup+390.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11988 0 0 0 38971 32 0 0 25 0 1 0 549967576 46637056 10609 4294967295 134512640 134672761 3221224544 3221197016 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11386 10609 603 41 0 11345 0 vsize: 45544 [startup+400.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11989 0 0 0 39971 32 0 0 25 0 1 0 549967576 46297088 10527 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11303 10527 603 41 0 11262 0 vsize: 45212 [startup+410.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11989 0 0 0 40971 32 0 0 25 0 1 0 549967576 46297088 10527 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11303 10527 603 41 0 11262 0 vsize: 45212 [startup+420.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11989 0 0 0 41971 32 0 0 25 0 1 0 549967576 46297088 10527 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11303 10527 603 41 0 11262 0 vsize: 45212 [startup+430.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11989 0 0 0 42972 32 0 0 25 0 1 0 549967576 46297088 10527 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11303 10527 603 41 0 11262 0 vsize: 45212 [startup+440.001 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 11990 0 0 0 43972 32 0 0 25 0 1 0 549967576 46297088 10528 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11303 10528 603 41 0 11262 0 vsize: 45212 [startup+450.001 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12163 0 0 0 44972 32 0 0 25 0 1 0 549967576 46321664 10560 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10560 603 41 0 11268 0 vsize: 45236 [startup+460.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12163 0 0 0 45972 32 0 0 25 0 1 0 549967576 46321664 10560 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10560 603 41 0 11268 0 vsize: 45236 [startup+470.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12163 0 0 0 46972 32 0 0 25 0 1 0 549967576 46321664 10560 4294967295 134512640 134672761 3221224544 3221222384 134597195 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10560 603 41 0 11268 0 vsize: 45236 [startup+480.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12163 0 0 0 47972 32 0 0 25 0 1 0 549967576 46321664 10560 4294967295 134512640 134672761 3221224544 3221222096 134597191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10560 603 41 0 11268 0 vsize: 45236 [startup+490.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12310 0 0 0 48972 32 0 0 25 0 1 0 549967576 46321664 10561 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10561 603 41 0 11268 0 vsize: 45236 [startup+500.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12310 0 0 0 49972 32 0 0 25 0 1 0 549967576 46321664 10561 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10561 603 41 0 11268 0 vsize: 45236 [startup+510.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12310 0 0 0 50972 32 0 0 25 0 1 0 549967576 46321664 10561 4294967295 134512640 134672761 3221224544 3221221664 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10561 603 41 0 11268 0 vsize: 45236 [startup+520.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12310 0 0 0 51972 32 0 0 25 0 1 0 549967576 46321664 10561 4294967295 134512640 134672761 3221224544 3221222384 134597212 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10561 603 41 0 11268 0 vsize: 45236 [startup+530.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12310 0 0 0 52973 32 0 0 25 0 1 0 549967576 46321664 10561 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11309 10561 603 41 0 11268 0 vsize: 45236 [startup+540.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12461 0 0 0 53972 33 0 0 25 0 1 0 549967576 46456832 10587 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10587 603 41 0 11301 0 vsize: 45368 [startup+550.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12461 0 0 0 54972 33 0 0 25 0 1 0 549967576 46456832 10587 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10587 603 41 0 11301 0 vsize: 45368 [startup+560.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12461 0 0 0 55973 33 0 0 25 0 1 0 549967576 46456832 10587 4294967295 134512640 134672761 3221224544 3221222096 134597167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10587 603 41 0 11301 0 vsize: 45368 [startup+570.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12461 0 0 0 56973 33 0 0 25 0 1 0 549967576 46456832 10587 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10587 603 41 0 11301 0 vsize: 45368 [startup+580.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12461 0 0 0 57973 33 0 0 25 0 1 0 549967576 46456832 10587 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10587 603 41 0 11301 0 vsize: 45368 [startup+590.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12463 0 0 0 58973 33 0 0 25 0 1 0 549967576 46456832 10589 4294967295 134512640 134672761 3221224544 3221223680 134560650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11342 10589 603 41 0 11301 0 vsize: 45368 [startup+600.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12687 0 0 0 59973 33 0 0 25 0 1 0 549967576 46608384 10634 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11379 10634 603 41 0 11338 0 vsize: 45516 [startup+610.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12687 0 0 0 60973 33 0 0 25 0 1 0 549967576 46608384 10634 4294967295 134512640 134672761 3221224544 3221222384 134597184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11379 10634 603 41 0 11338 0 vsize: 45516 [startup+620.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12687 0 0 0 61973 33 0 0 25 0 1 0 549967576 46608384 10634 4294967295 134512640 134672761 3221224544 3221222528 134597262 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11379 10634 603 41 0 11338 0 vsize: 45516 [startup+630.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12687 0 0 0 62974 33 0 0 25 0 1 0 549967576 46608384 10634 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11379 10634 603 41 0 11338 0 vsize: 45516 [startup+640.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12688 0 0 0 63974 33 0 0 25 0 1 0 549967576 46608384 10635 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11379 10635 603 41 0 11338 0 vsize: 45516 [startup+650.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12765 0 0 0 64974 33 0 0 25 0 1 0 549967576 47009792 10712 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11477 10712 603 41 0 11436 0 vsize: 45908 [startup+660.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 12911 0 0 0 65974 33 0 0 25 0 1 0 549967576 47546368 10858 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11608 10858 603 41 0 11567 0 vsize: 46432 [startup+670.002 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13200 0 0 0 66973 34 0 0 25 0 1 0 549967576 47951872 10968 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11707 10968 603 41 0 11666 0 vsize: 46828 [startup+680.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13200 0 0 0 67973 34 0 0 25 0 1 0 549967576 47951872 10968 4294967295 134512640 134672761 3221224544 3221222096 134597191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11707 10968 603 41 0 11666 0 vsize: 46828 [startup+690.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13200 0 0 0 68974 34 0 0 25 0 1 0 549967576 47951872 10968 4294967295 134512640 134672761 3221224544 3221222816 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11707 10968 603 41 0 11666 0 vsize: 46828 [startup+700.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13200 0 0 0 69974 34 0 0 25 0 1 0 549967576 47951872 10968 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11707 10968 603 41 0 11666 0 vsize: 46828 [startup+710.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13203 0 0 0 70974 34 0 0 25 0 1 0 549967576 47951872 10968 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11707 10968 603 41 0 11666 0 vsize: 46828 [startup+720.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13408 0 0 0 71974 34 0 0 25 0 1 0 549967576 48029696 10988 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 10988 603 41 0 11685 0 vsize: 46904 [startup+730.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13408 0 0 0 72974 34 0 0 25 0 1 0 549967576 48029696 10988 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 10988 603 41 0 11685 0 vsize: 46904 [startup+740.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13408 0 0 0 73974 34 0 0 25 0 1 0 549967576 48029696 10988 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 10988 603 41 0 11685 0 vsize: 46904 [startup+750.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13408 0 0 0 74975 34 0 0 25 0 1 0 549967576 48029696 10988 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 10988 603 41 0 11685 0 vsize: 46904 [startup+760.005 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13413 0 0 0 75975 35 0 0 25 0 1 0 549967576 48029696 10989 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 10989 603 41 0 11685 0 vsize: 46904 [startup+770.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13645 0 0 0 76974 35 0 0 25 0 1 0 549967576 48304128 11046 4294967295 134512640 134672761 3221224544 3221222240 134597184 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11793 11046 603 41 0 11752 0 vsize: 47172 [startup+780.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13645 0 0 0 77974 35 0 0 25 0 1 0 549967576 48304128 11046 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11793 11046 603 41 0 11752 0 vsize: 47172 [startup+790.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13645 0 0 0 78975 35 0 0 25 0 1 0 549967576 48304128 11046 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11793 11046 603 41 0 11752 0 vsize: 47172 [startup+800.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13645 0 0 0 79975 35 0 0 25 0 1 0 549967576 48304128 11046 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11793 11046 603 41 0 11752 0 vsize: 47172 [startup+810.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13646 0 0 0 80975 35 0 0 25 0 1 0 549967576 48304128 11047 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11793 11047 603 41 0 11752 0 vsize: 47172 [startup+820.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13833 0 0 0 81974 36 0 0 25 0 1 0 549967576 48316416 11051 4294967295 134512640 134672761 3221224544 3221221808 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11796 11051 603 41 0 11755 0 vsize: 47184 [startup+830.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13833 0 0 0 82975 36 0 0 25 0 1 0 549967576 48316416 11051 4294967295 134512640 134672761 3221224544 3221222384 134597176 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11796 11051 603 41 0 11755 0 vsize: 47184 [startup+840.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13833 0 0 0 83975 36 0 0 25 0 1 0 549967576 48316416 11051 4294967295 134512640 134672761 3221224544 3221222384 134597191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11796 11051 603 41 0 11755 0 vsize: 47184 [startup+850.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13833 0 0 0 84975 36 0 0 25 0 1 0 549967576 48316416 11051 4294967295 134512640 134672761 3221224544 3221222064 1075349719 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11796 11051 603 41 0 11755 0 vsize: 47184 [startup+860.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 13837 0 0 0 85975 36 0 0 25 0 1 0 549967576 48316416 11051 4294967295 134512640 134672761 3221224544 3221223728 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11796 11051 603 41 0 11755 0 vsize: 47184 [startup+870.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14067 0 0 0 86974 37 0 0 25 0 1 0 549967576 48500736 11097 4294967295 134512640 134672761 3221224544 3221222112 1075352443 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11841 11097 603 41 0 11800 0 vsize: 47364 [startup+880.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14067 0 0 0 87975 37 0 0 25 0 1 0 549967576 48500736 11097 4294967295 134512640 134672761 3221224544 3221221776 134522368 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11841 11097 603 41 0 11800 0 vsize: 47364 [startup+890.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14067 0 0 0 88975 37 0 0 25 0 1 0 549967576 48500736 11097 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11841 11097 603 41 0 11800 0 vsize: 47364 [startup+900.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14067 0 0 0 89975 37 0 0 25 0 1 0 549967576 48500736 11097 4294967295 134512640 134672761 3221224544 3221221520 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11841 11097 603 41 0 11800 0 vsize: 47364 [startup+910.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14070 0 0 0 90975 37 0 0 25 0 1 0 549967576 48500736 11097 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11841 11097 603 41 0 11800 0 vsize: 47364 [startup+920.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14090 0 0 0 91975 37 0 0 25 0 1 0 549967576 48631808 11117 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11873 11117 603 41 0 11832 0 vsize: 47492 [startup+930.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14308 0 0 0 92975 37 0 0 25 0 1 0 549967576 48730112 11154 4294967295 134512640 134672761 3221224544 3221221808 134597218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11897 11154 603 41 0 11856 0 vsize: 47588 [startup+940.004 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14308 0 0 0 93975 37 0 0 25 0 1 0 549967576 48730112 11154 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11897 11154 603 41 0 11856 0 vsize: 47588 [startup+950.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14308 0 0 0 94975 37 0 0 25 0 1 0 549967576 48730112 11154 4294967295 134512640 134672761 3221224544 3221222672 134597237 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11897 11154 603 41 0 11856 0 vsize: 47588 [startup+960.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 14308 0 0 0 95975 37 0 0 25 0 1 0 549967576 48730112 11154 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11897 11154 603 41 0 11856 0 vsize: 47588 [startup+970.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 20678 0 0 0 96962 51 0 0 25 0 1 0 549967576 79155200 17194 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19325 17194 603 41 0 19284 0 vsize: 77300 [startup+980.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 20718 0 0 0 97962 51 0 0 25 0 1 0 549967576 79417344 17234 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19389 17234 603 41 0 19348 0 vsize: 77556 [startup+990.003 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21065 0 0 0 98961 52 0 0 25 0 1 0 549967576 80338944 17456 4294967295 134512640 134672761 3221224544 3221221580 1075350064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19614 17456 603 41 0 19573 0 vsize: 78456 [startup+1000 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21065 0 0 0 99962 52 0 0 25 0 1 0 549967576 80338944 17456 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19614 17456 603 41 0 19573 0 vsize: 78456 [startup+1010 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21065 0 0 0 100962 52 0 0 25 0 1 0 549967576 80338944 17456 4294967295 134512640 134672761 3221224544 3221221808 134597225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19614 17456 603 41 0 19573 0 vsize: 78456 [startup+1020 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21065 0 0 0 101962 52 0 0 25 0 1 0 549967576 80338944 17456 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19614 17456 603 41 0 19573 0 vsize: 78456 [startup+1030 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21071 0 0 0 102962 52 0 0 25 0 1 0 549967576 80338944 17462 4294967295 134512640 134672761 3221224544 3221223668 134566133 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19614 17462 603 41 0 19573 0 vsize: 78456 [startup+1040 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21229 0 0 0 103962 52 0 0 25 0 1 0 549967576 80429056 17491 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19636 17491 603 41 0 19595 0 vsize: 78544 [startup+1050 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21229 0 0 0 104962 52 0 0 25 0 1 0 549967576 80429056 17491 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19636 17491 603 41 0 19595 0 vsize: 78544 [startup+1060 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21229 0 0 0 105962 52 0 0 25 0 1 0 549967576 80429056 17491 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19636 17491 603 41 0 19595 0 vsize: 78544 [startup+1070 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21229 0 0 0 106963 52 0 0 25 0 1 0 549967576 80429056 17491 4294967295 134512640 134672761 3221224544 3221221952 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19636 17491 603 41 0 19595 0 vsize: 78544 [startup+1080 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21229 0 0 0 107963 52 0 0 25 0 1 0 549967576 80429056 17491 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19636 17491 603 41 0 19595 0 vsize: 78544 [startup+1090 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21309 0 0 0 108963 52 0 0 25 0 1 0 549967576 80953344 17571 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19764 17571 603 41 0 19723 0 vsize: 79056 [startup+1100 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21462 0 0 0 109962 52 0 0 25 0 1 0 549967576 81088512 17599 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17599 603 41 0 19756 0 vsize: 79188 [startup+1110 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21462 0 0 0 110963 52 0 0 25 0 1 0 549967576 81088512 17599 4294967295 134512640 134672761 3221224544 3221222240 134597195 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17599 603 41 0 19756 0 vsize: 79188 [startup+1120 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21462 0 0 0 111963 52 0 0 25 0 1 0 549967576 81088512 17599 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17599 603 41 0 19756 0 vsize: 79188 [startup+1130 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21462 0 0 0 112963 52 0 0 25 0 1 0 549967576 81088512 17599 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17599 603 41 0 19756 0 vsize: 79188 [startup+1140 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21463 0 0 0 113963 53 0 0 25 0 1 0 549967576 81088512 17600 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17600 603 41 0 19756 0 vsize: 79188 [startup+1150 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21464 0 0 0 114963 53 0 0 25 0 1 0 549967576 81088512 17601 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19797 17601 603 41 0 19756 0 vsize: 79188 [startup+1160 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21528 0 0 0 115963 53 0 0 25 0 1 0 549967576 81350656 17665 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19861 17665 603 41 0 19820 0 vsize: 79444 [startup+1170 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21758 0 0 0 116963 53 0 0 25 0 1 0 549967576 81522688 17714 4294967295 134512640 134672761 3221224544 3221221664 134597200 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19903 17714 603 41 0 19862 0 vsize: 79612 [startup+1180 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21758 0 0 0 117963 53 0 0 25 0 1 0 549967576 81522688 17714 4294967295 134512640 134672761 3221224544 3221222240 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19903 17714 603 41 0 19862 0 vsize: 79612 [startup+1190 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21758 0 0 0 118963 53 0 0 25 0 1 0 549967576 81522688 17714 4294967295 134512640 134672761 3221224544 3221222096 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19903 17714 603 41 0 19862 0 vsize: 79612 [startup+1200 s] Raw data (loadavg): 0.99 0.99 0.99 2/54 4275 Raw data (stat): 4273 (minisat+) R 4272 10614 10613 0 -1 0 21758 0 0 0 119963 53 0 0 25 0 1 0 549967576 81522688 17714 4294967295 134512640 134672761 3221224544 3221222384 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19903 17714 603 41 0 19862 0 vsize: 79612 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.04 s] Raw data (loadavg): 0.99 0.99 0.99 1/54 4275 Raw data (stat): 4273 (minisat+) Z 4272 10614 10613 0 -1 12 21761 0 0 0 119964 57 0 0 25 0 1 0 549967576 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.04 CPU time (s): 1200.21 CPU user time (s): 1199.64 CPU system time (s): 0.573912 CPU usage (%): 100.015 Max. virtual memory (Kb): 79612 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####