Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0201.opb |
MD5SUM | 8c361d02d5162bb0b133ab6ed38f9294 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1523 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 201 |
Biggest coefficient in the objective function | 1920 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 19980 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 1920 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 19980 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 201 |
Total number of constraints | 334 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 227 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 67 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc5 THE 2005-04-21 22:54:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=13712 boxname=wulflinc5 idbench=1055 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c361d02d5162bb0b133ab6ed38f9294 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-p0201.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-p0201.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-p0201.opb IDLAUNCH: 13712 /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: 577552 kB Buffers: 28788 kB Cached: 407396 kB SwapCached: 444 kB Active: 83128 kB Inactive: 355216 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 577300 kB SwapTotal: 2097136 kB SwapFree: 2095948 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5200 kB Slab: 12964 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 23:15:00 (client local time) WITH STATUS 10 IN 1200.23 SECONDS stats: 13712 7 1200.23 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 133 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): sssss c ---[ 137]---> Adder-cost: 7 maxlim: 5 bits: 4/3 c ---[ 136]---> Adder-cost: 7 maxlim: 5 bits: 4/3 c ---[ 135]---> Adder-cost: 7 maxlim: 5 bits: 4/3 c ---[ 133]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 131]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 129]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 127]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 125]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 123]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 121]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 119]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 117]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 115]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 113]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 111]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 109]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 107]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 105]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 103]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 101]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 99]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 97]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 95]---> Adder-cost: 11 maxlim: 1 bits: 2/1 c ---[ 89]---> Adder-cost: 42 maxlim: 9 bits: 5/4 c ---[ 88]---> Adder-cost: 62 maxlim: 14 bits: 5/4 c ---[ 87]---> Adder-cost: 62 maxlim: 14 bits: 5/4 c ---[ 86]---> Adder-cost: 45 maxlim: 14 bits: 5/4 c ---[ 85]---> Adder-cost: 53 maxlim: 19 bits: 6/5 c ---[ 84]---> Adder-cost: 53 maxlim: 19 bits: 6/5 c ---[ 83]---> Adder-cost: 57 maxlim: 19 bits: 6/5 c ---[ 82]---> Adder-cost: 57 maxlim: 24 bits: 6/5 c ---[ 81]---> Adder-cost: 57 maxlim: 24 bits: 6/5 c ---[ 80]---> Adder-cost: 64 maxlim: 24 bits: 6/5 c ---[ 79]---> Adder-cost: 65 maxlim: 29 bits: 6/5 c ---[ 78]---> Adder-cost: 65 maxlim: 29 bits: 6/5 c ---[ 77]---> Adder-cost: 71 maxlim: 29 bits: 6/5 c ---[ 76]---> Adder-cost: 82 maxlim: 34 bits: 7/6 c ---[ 75]---> Adder-cost: 82 maxlim: 34 bits: 7/6 c ---[ 74]---> Adder-cost: 80 maxlim: 34 bits: 7/6 c ---[ 73]---> Adder-cost: 78 maxlim: 39 bits: 7/6 c ---[ 72]---> Adder-cost: 78 maxlim: 39 bits: 7/6 c ---[ 71]---> Adder-cost: 83 maxlim: 39 bits: 7/6 c ---[ 70]---> Adder-cost: 95 maxlim: 44 bits: 7/6 c ---[ 69]---> Adder-cost: 95 maxlim: 44 bits: 7/6 c ---[ 68]---> Adder-cost: 99 maxlim: 44 bits: 7/6 c ---[ 67]---> Adder-cost: 91 maxlim: 49 bits: 7/6 c ---[ 66]---> Adder-cost: 91 maxlim: 49 bits: 7/6 c ---[ 65]---> Adder-cost: 100 maxlim: 49 bits: 7/6 c ---[ 64]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 63]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 62]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 61]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 60]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 59]---> Adder-cost: 2 maxlim: 1 bits: 2/1 c ---[ 58]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 57]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 56]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 55]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 54]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 53]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 52]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 51]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 50]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 49]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 48]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 47]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 46]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 45]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 44]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 43]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 42]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 41]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 40]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 39]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 38]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 37]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 36]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 35]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 34]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 33]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 32]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 31]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 30]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 29]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 28]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 27]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 26]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 25]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 24]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 23]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 22]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 21]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 20]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 19]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 18]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 17]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 16]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 15]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 14]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 13]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 12]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 11]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 10]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 9]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 8]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 7]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 6]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 5]---> Adder-cost: 6 maxlim: 2 bits: 3/2 c ---[ 4]---> Adder-cost: 6 maxlim: 4 bits: 4/3 c ---[ 3]---> Adder-cost: 6 maxlim: 4 bits: 4/3 c ---[ 2]---> Adder-cost: 6 maxlim: 4 bits: 4/3 c ---[ 1]---> Adder-cost: 6 maxlim: 9 bits: 5/4 c ---[ 0]---> Adder-cost: 6 maxlim: 9 bits: 5/4 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 13192 46987 | 4397 0 0 nan | 0.000 % | c | 102 | 13165 46890 | 4836 100 512 5.1 | 13.328 % | c | 252 | 13165 46890 | 5320 250 1591 6.4 | 13.328 % | c | 478 | 13096 46639 | 5852 462 2805 6.1 | 13.441 % | c | 817 | 13046 46459 | 6437 796 4934 6.2 | 13.517 % | c ============================================================================== c [1mFound solution: 2428[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 1154 maxlim: 12752 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1226 | 20917 74551 | 6972 1183 9347 7.9 | 13.517 % | c ============================================================================== c [1mFound solution: 2162[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13018 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1284 | 20935 74652 | 6978 1241 10250 8.3 | 13.517 % | c | 1385 | 20897 74522 | 7675 1330 11268 8.5 | 10.120 % | c | 1535 | 20897 74522 | 8443 1480 16368 11.1 | 10.120 % | c | 1761 | 20877 74453 | 9287 1703 20933 12.3 | 10.225 % | c | 2098 | 20877 74453 | 10216 2040 49761 24.4 | 10.225 % | c | 2605 | 20863 74406 | 11238 2544 69218 27.2 | 10.330 % | c ============================================================================== c [1mFound solution: 1947[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13233 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3053 | 20861 74423 | 6953 2991 82792 27.7 | 10.330 % | c | 3153 | 20834 74322 | 7648 3084 83775 27.2 | 10.525 % | c | 3303 | 20834 74322 | 8413 3234 92849 28.7 | 10.525 % | c | 3528 | 20834 74322 | 9254 3459 100051 28.9 | 10.525 % | c | 3865 | 20834 74322 | 10179 3796 106126 28.0 | 10.525 % | c | 4372 | 20834 74322 | 11197 4303 141217 32.8 | 10.525 % | c | 5131 | 20834 74322 | 12317 5062 175900 34.7 | 10.525 % | c | 6270 | 20834 74322 | 13549 6201 226014 36.4 | 10.525 % | c | 7978 | 20834 74322 | 14904 7909 318227 40.2 | 10.525 % | c | 10541 | 20815 74257 | 16394 10470 452111 43.2 | 10.577 % | c | 14385 | 20806 74226 | 18034 14308 674649 47.2 | 10.603 % | c | 20151 | 20797 74195 | 19837 10130 594184 58.7 | 10.629 % | c ============================================================================== c [1mFound solution: 1941[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13239 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20652 | 20798 74205 | 6932 10631 618925 58.2 | 10.629 % | c | 20755 | 20798 74205 | 7625 5419 298843 55.1 | 10.653 % | c | 20905 | 20798 74205 | 8387 5569 302559 54.3 | 10.653 % | c | 21135 | 20733 73974 | 9226 5792 305866 52.8 | 10.757 % | c | 21472 | 20733 73974 | 10149 6129 323193 52.7 | 10.757 % | c ============================================================================== c [1mFound solution: 1881[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13299 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21663 | 20729 73980 | 6909 6314 326921 51.8 | 10.757 % | c | 21764 | 20729 73980 | 7599 6415 328460 51.2 | 10.874 % | c | 21914 | 20729 73980 | 8359 6565 331126 50.4 | 10.874 % | c | 22140 | 20729 73980 | 9195 6791 335685 49.4 | 10.874 % | c | 22478 | 20729 73980 | 10115 7129 344075 48.3 | 10.874 % | c | 22984 | 20729 73980 | 11127 7635 371537 48.7 | 10.874 % | c | 23746 | 20729 73980 | 12239 8397 400269 47.7 | 10.874 % | c | 24886 | 20729 73980 | 13463 9537 458097 48.0 | 10.874 % | c | 26596 | 20729 73980 | 14810 11247 536502 47.7 | 10.874 % | c | 29158 | 20729 73980 | 16291 13809 672019 48.7 | 10.874 % | c | 33003 | 20729 73980 | 17920 8861 315812 35.6 | 10.874 % | c | 38770 | 20729 73980 | 19712 14628 696358 47.6 | 10.874 % | c | 47422 | 20729 73980 | 21683 12478 962229 77.1 | 10.874 % | c | 60401 | 20720 73949 | 23851 13731 1249003 91.0 | 10.900 % | c ============================================================================== c [1mFound solution: 1845[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13335 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 79201 | 20710 73927 | 6903 19943 1158596 58.1 | 10.900 % | c | 79301 | 20701 73896 | 7593 5081 208581 41.1 | 11.071 % | c | 79455 | 20701 73896 | 8352 5235 211500 40.4 | 11.071 % | c | 79683 | 20701 73896 | 9187 5463 215382 39.4 | 11.071 % | c | 80020 | 20608 73570 | 10106 5782 226786 39.2 | 11.383 % | c | 80526 | 20608 73570 | 11117 6288 256199 40.7 | 11.383 % | c | 81285 | 20608 73570 | 12229 7047 284205 40.3 | 11.383 % | c | 82424 | 20608 73570 | 13451 8186 347258 42.4 | 11.383 % | c | 84133 | 20608 73570 | 14797 9895 437901 44.3 | 11.383 % | c | 86695 | 20608 73570 | 16276 12457 677783 54.4 | 11.383 % | c ============================================================================== c [1mFound solution: 1792[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13388 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 89854 | 20616 73627 | 6872 15616 849559 54.4 | 11.383 % | c | 89954 | 20616 73627 | 7559 4004 123632 30.9 | 11.475 % | c | 90104 | 20616 73627 | 8315 4154 126972 30.6 | 11.475 % | c | 90330 | 20616 73627 | 9146 4380 143530 32.8 | 11.475 % | c | 90667 | 20616 73627 | 10061 4717 156029 33.1 | 11.475 % | c | 91174 | 20616 73627 | 11067 5224 197057 37.7 | 11.475 % | c | 91933 | 20616 73627 | 12174 5983 231832 38.7 | 11.475 % | c | 93072 | 20616 73627 | 13391 7122 298894 42.0 | 11.475 % | c | 94781 | 20601 73576 | 14730 8829 376707 42.7 | 11.527 % | c | 97344 | 20580 73507 | 16203 11389 507705 44.6 | 11.736 % | c | 101188 | 20580 73507 | 17824 15233 713304 46.8 | 11.736 % | c | 106958 | 20573 73484 | 19606 11111 540489 48.6 | 11.762 % | c | 115607 | 20573 73484 | 21567 19760 1194727 60.5 | 11.762 % | c ============================================================================== c [1mFound solution: 1781[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13399 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 123379 | 20577 73506 | 6859 16112 1044981 64.9 | 11.762 % | c | 123480 | 20577 73506 | 7544 4129 179466 43.5 | 11.801 % | c | 123630 | 20577 73506 | 8299 4279 183631 42.9 | 11.801 % | c ============================================================================== c [1mFound solution: 1776[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13404 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 123739 | 20574 73512 | 6858 4385 185485 42.3 | 11.801 % | c | 123839 | 20574 73512 | 7543 4485 186639 41.6 | 11.870 % | c | 123989 | 20574 73512 | 8298 4635 189401 40.9 | 11.870 % | c | 124215 | 20574 73512 | 9127 4861 201143 41.4 | 11.870 % | c | 124552 | 20574 73512 | 10040 5198 208179 40.0 | 11.870 % | c | 125059 | 20574 73512 | 11044 5705 224862 39.4 | 11.870 % | c | 125818 | 20574 73512 | 12149 6464 252405 39.0 | 11.870 % | c | 126958 | 20574 73512 | 13364 7604 319283 42.0 | 11.870 % | c | 128666 | 20574 73512 | 14700 9312 379315 40.7 | 11.870 % | c | 131228 | 20574 73512 | 16170 11874 507598 42.7 | 11.870 % | c | 135072 | 20574 73512 | 17787 15718 699107 44.5 | 11.870 % | c | 140838 | 20574 73512 | 19566 12194 511648 42.0 | 11.870 % | c | 149488 | 20574 73512 | 21523 20844 1145270 54.9 | 11.870 % | c | 162464 | 20574 73512 | 23675 11598 357808 30.9 | 11.870 % | c | 181925 | 20574 73512 | 26043 18603 870687 46.8 | 11.870 % | c | 211118 | 20560 73469 | 28647 20308 950919 46.8 | 12.026 % | c ============================================================================== c [1mFound solution: 1755[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13425 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 218305 | 20558 73479 | 6852 27494 1360587 49.5 | 12.026 % | c | 218405 | 20558 73479 | 7537 6974 282225 40.5 | 12.114 % | c | 218555 | 20558 73479 | 8290 7124 291456 40.9 | 12.114 % | c | 218780 | 20558 73479 | 9120 7349 297264 40.4 | 12.114 % | c | 219118 | 20558 73479 | 10032 7687 312851 40.7 | 12.114 % | c | 219624 | 20543 73428 | 11035 8192 333718 40.7 | 12.166 % | c | 220385 | 20543 73428 | 12138 8953 364519 40.7 | 12.166 % | c | 221524 | 20543 73428 | 13352 10092 445827 44.2 | 12.166 % | c | 223235 | 20543 73428 | 14687 11803 506621 42.9 | 12.166 % | c ============================================================================== c [1mFound solution: 1753[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13427 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 224071 | 20545 73441 | 6848 12639 570718 45.2 | 12.166 % | c | 224174 | 20545 73441 | 7532 6423 229446 35.7 | 12.186 % | c | 224325 | 20545 73441 | 8286 6574 231335 35.2 | 12.186 % | c | 224550 | 20545 73441 | 9114 6799 241235 35.5 | 12.186 % | c | 224887 | 20545 73441 | 10026 7136 257151 36.0 | 12.186 % | c | 225393 | 20545 73441 | 11028 7642 277215 36.3 | 12.186 % | c | 226153 | 20545 73441 | 12131 8402 312015 37.1 | 12.186 % | c | 227292 | 20534 73402 | 13344 9534 369422 38.7 | 12.237 % | c | 229000 | 20534 73402 | 14679 11242 449302 40.0 | 12.237 % | c | 231563 | 20513 73333 | 16147 13801 552988 40.1 | 12.445 % | c | 235411 | 20513 73333 | 17761 8871 358458 40.4 | 12.445 % | c | 241177 | 20513 73333 | 19538 14637 660248 45.1 | 12.445 % | c | 249826 | 20513 73333 | 21491 12851 614043 47.8 | 12.445 % | c ============================================================================== c [1mFound solution: 1749[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13431 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 253344 | 20515 73345 | 6838 16369 868856 53.1 | 12.445 % | c | 253444 | 20515 73345 | 7521 4193 183263 43.7 | 12.464 % | c | 253596 | 20515 73345 | 8273 4345 185094 42.6 | 12.464 % | c | 253821 | 20515 73345 | 9101 4570 194627 42.6 | 12.464 % | c | 254158 | 20515 73345 | 10011 4907 203451 41.5 | 12.464 % | c | 254665 | 20501 73300 | 11012 5410 234658 43.4 | 12.594 % | c | 255424 | 20392 72907 | 12113 6163 262281 42.6 | 12.724 % | c | 256569 | 20392 72907 | 13325 7308 322651 44.2 | 12.724 % | c | 258277 | 20392 72907 | 14657 9016 417101 46.3 | 12.724 % | c | 260839 | 20392 72907 | 16123 11578 564920 48.8 | 12.724 % | c | 264683 | 20392 72907 | 17736 15422 817769 53.0 | 12.724 % | c | 270449 | 20392 72907 | 19509 11603 556279 47.9 | 12.724 % | c | 279098 | 20392 72907 | 21460 20252 1002558 49.5 | 12.724 % | c | 292075 | 20385 72884 | 23606 21612 1253343 58.0 | 12.749 % | c | 311536 | 20385 72884 | 25967 15413 1163512 75.5 | 12.749 % | c | 340728 | 20378 72860 | 28564 17676 914637 51.7 | 12.827 % | c ============================================================================== c [1mFound solution: 1747[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13433 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 348975 | 20380 72874 | 6793 25923 1421789 54.8 | 12.827 % | c | 349075 | 20380 72874 | 7472 6581 280029 42.6 | 12.846 % | c | 349226 | 20380 72874 | 8219 6732 282796 42.0 | 12.846 % | c | 349451 | 20380 72874 | 9041 6957 297001 42.7 | 12.846 % | c | 349788 | 20380 72874 | 9945 7294 308706 42.3 | 12.846 % | c | 350296 | 20380 72874 | 10940 7802 344058 44.1 | 12.846 % | c | 351056 | 20380 72874 | 12034 8562 385330 45.0 | 12.846 % | c | 352195 | 20380 72874 | 13237 9701 437147 45.1 | 12.846 % | c | 353903 | 20380 72874 | 14561 11409 601799 52.7 | 12.846 % | c | 356467 | 20380 72874 | 16017 13973 802605 57.4 | 12.846 % | c | 360312 | 20358 72800 | 17619 9252 444555 48.0 | 12.924 % | c | 366078 | 20357 72796 | 19381 15015 634731 42.3 | 12.950 % | c | 374728 | 20335 72720 | 21319 13215 555286 42.0 | 13.002 % | c | 387702 | 20335 72720 | 23451 15014 734359 48.9 | 13.002 % | c | 407163 | 20335 72720 | 25796 22068 1444824 65.5 | 13.002 % | c | 436355 | 20328 72697 | 28376 23909 1530806 64.0 | 13.028 % | c | 480144 | 20321 72675 | 31213 22853 1559072 68.2 | 13.131 % | c | 545828 | 20307 72630 | 34335 20039 1082279 54.0 | 13.261 % | c ============================================================================== c [1mFound solution: 1731[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13449 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 567573 | 20312 72662 | 6770 20925 1488167 71.1 | 13.261 % | c | 567673 | 20312 72662 | 7447 5332 308185 57.8 | 13.321 % | c | 567823 | 20312 72662 | 8191 5482 316939 57.8 | 13.321 % | c | 568048 | 20312 72662 | 9010 5707 327787 57.4 | 13.321 % | c | 568385 | 20312 72662 | 9911 6044 342106 56.6 | 13.321 % | c | 568891 | 20312 72662 | 10903 6550 355578 54.3 | 13.321 % | c | 569652 | 20312 72662 | 11993 7311 376668 51.5 | 13.321 % | c | 570791 | 20312 72662 | 13192 8450 446785 52.9 | 13.321 % | c | 572500 | 20312 72662 | 14512 10159 562957 55.4 | 13.321 % | c | 575062 | 20291 72594 | 15963 12716 672193 52.9 | 13.476 % | c | 578906 | 20291 72594 | 17559 16560 920761 55.6 | 13.476 % | c | 584672 | 20291 72594 | 19315 13162 599136 45.5 | 13.476 % | c | 593322 | 20284 72571 | 21247 11852 532807 45.0 | 13.502 % | c | 606297 | 20284 72571 | 23371 13541 691950 51.1 | 13.502 % | c | 625758 | 20284 72571 | 25709 20744 1225003 59.1 | 13.502 % | c | 654954 | 20263 72503 | 28279 22999 1116401 48.5 | 13.658 % | c ============================================================================== c [1mFound solution: 1591[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 13589 bits: 14/14 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 685274 | 20269 72544 | 6756 23990 1270883 53.0 | 13.658 % | c | 685374 | 20269 72544 | 7431 6098 174802 28.7 | 13.740 % | c | 685524 | 20269 72544 | 8174 6248 186081 29.8 | 13.740 % | c | 685749 | 20269 72544 | 8992 6473 192806 29.8 | 13.740 % | c | 686091 | 20269 72544 | 9891 6815 207068 30.4 | 13.740 % | c | 686598 | 20269 72544 | 10880 7322 236326 32.3 | 13.740 % | c | 687357 | 20269 72544 | 11968 8081 280887 34.8 | 13.740 % | c | 688498 | 20269 72544 | 13165 9222 329454 35.7 | 13.740 % | c | 690208 | 20262 72521 | 14482 10931 398941 36.5 | 13.766 % | c | 692770 | 20262 72521 | 15930 13493 520308 38.6 | 13.766 % | c | 696615 | 20262 72521 | 17523 8889 260805 29.3 | 13.766 % | c | 702381 | 20262 72521 | 19275 14655 661771 45.2 | 13.766 % | c | 711030 | 20262 72521 | 21203 13238 639875 48.3 | 13.766 % | c | 724005 | 20262 72521 | 23323 14574 978289 67.1 | 13.766 % | c | 743468 | 20262 72521 | 25655 21757 1341594 61.7 | 13.766 % | c | 772660 | 20262 72521 | 28221 24078 1777531 73.8 | 13.766 % | c | 816449 | 20262 72521 | 31043 24006 1304022 54.3 | 13.766 % | c | 882134 | 20262 72521 | 34148 25166 1692918 67.3 | 13.766 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.91 0.95 0.97 2/54 3062 Raw data (stat): 3062 (runsolver) R 3061 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490619640 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0001 s] Raw data (loadavg): 0.92 0.95 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 1621 0 0 0 994 5 0 0 25 0 1 0 490619640 8228864 1599 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2009 1599 603 41 0 1968 0 vsize: 8036 [startup+20.0013 s] Raw data (loadavg): 0.93 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 1988 0 0 0 1992 6 0 0 25 0 1 0 490619640 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2405 1966 603 41 0 2364 0 vsize: 9620 [startup+30.0026 s] Raw data (loadavg): 0.94 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 1988 0 0 0 2992 6 0 0 25 0 1 0 490619640 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2405 1966 603 41 0 2364 0 vsize: 9620 [startup+40.0024 s] Raw data (loadavg): 0.95 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 2284 0 0 0 3991 8 0 0 25 0 1 0 490619640 11055104 2262 4294967295 134512640 134672761 3221224544 3221223648 134560303 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2699 2262 603 41 0 2658 0 vsize: 10796 [startup+50.0025 s] Raw data (loadavg): 0.96 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 2446 0 0 0 4991 8 0 0 25 0 1 0 490619640 11730944 2424 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2864 2424 603 41 0 2823 0 vsize: 11456 [startup+60.0028 s] Raw data (loadavg): 0.96 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3100 0 0 0 5989 10 0 0 25 0 1 0 490619640 14413824 3078 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3519 3078 603 41 0 3478 0 vsize: 14076 [startup+70.0036 s] Raw data (loadavg): 0.97 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3100 0 0 0 6989 10 0 0 25 0 1 0 490619640 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134561115 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3519 3078 603 41 0 3478 0 vsize: 14076 [startup+80.0048 s] Raw data (loadavg): 0.97 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3101 0 0 0 7989 11 0 0 25 0 1 0 490619640 14401536 3079 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3079 603 41 0 3475 0 vsize: 14064 [startup+90.0051 s] Raw data (loadavg): 0.98 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 8989 11 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+100.005 s] Raw data (loadavg): 0.98 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 9988 11 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+110.006 s] Raw data (loadavg): 0.98 0.96 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 10988 11 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+120.006 s] Raw data (loadavg): 0.98 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 11988 11 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+130.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 12989 11 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+140.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 13988 12 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134559910 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+150.008 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 14988 12 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 15988 12 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 16988 12 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 17988 12 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 18988 13 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3102 0 0 0 19987 13 0 0 25 0 1 0 490619640 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3292 0 0 0 20987 14 0 0 25 0 1 0 490619640 15069184 3270 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3679 3270 603 41 0 3638 0 vsize: 14716 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3320 0 0 0 21987 14 0 0 25 0 1 0 490619640 15204352 3298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3712 3298 603 41 0 3671 0 vsize: 14848 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3332 0 0 0 22986 15 0 0 25 0 1 0 490619640 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3310 603 41 0 3704 0 vsize: 14980 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3332 0 0 0 23986 15 0 0 25 0 1 0 490619640 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134553605 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3310 603 41 0 3704 0 vsize: 14980 [startup+250.011 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3333 0 0 0 24986 15 0 0 25 0 1 0 490619640 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3333 0 0 0 25985 16 0 0 25 0 1 0 490619640 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+270.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3333 0 0 0 26985 16 0 0 25 0 1 0 490619640 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 27985 17 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+290.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 28985 17 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+300.014 s] Raw data (loadavg): 0.99 0.97 0.97 2/54 3062 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 29985 17 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+310.014 s] Raw data (loadavg): 1.07 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 30983 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+320.014 s] Raw data (loadavg): 1.06 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 31984 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+330.015 s] Raw data (loadavg): 1.05 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 32984 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+340.015 s] Raw data (loadavg): 1.04 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 33984 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+350.015 s] Raw data (loadavg): 1.04 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 34984 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223648 134555357 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+360.016 s] Raw data (loadavg): 1.03 0.99 0.98 2/54 3115 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 35984 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+370.016 s] Raw data (loadavg): 1.03 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 36985 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+380.017 s] Raw data (loadavg): 1.02 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 37985 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223728 134559055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+390.016 s] Raw data (loadavg): 1.02 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 38985 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+400.016 s] Raw data (loadavg): 1.01 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 39985 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+410.017 s] Raw data (loadavg): 1.01 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 40985 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+420.025 s] Raw data (loadavg): 1.01 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 41986 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+430.026 s] Raw data (loadavg): 1.01 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 42986 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+440.026 s] Raw data (loadavg): 1.01 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 43987 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+450.026 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3334 0 0 0 44987 18 0 0 25 0 1 0 490619640 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+460.026 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3450 0 0 0 45986 18 0 0 25 0 1 0 490619640 15736832 3428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3842 3428 603 41 0 3801 0 vsize: 15368 [startup+470.03 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3450 0 0 0 46987 18 0 0 25 0 1 0 490619640 15736832 3428 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3842 3428 603 41 0 3801 0 vsize: 15368 [startup+480.03 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3549 0 0 0 47987 19 0 0 25 0 1 0 490619640 16138240 3527 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3527 603 41 0 3899 0 vsize: 15760 [startup+490.038 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3549 0 0 0 48988 19 0 0 25 0 1 0 490619640 16138240 3527 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3527 603 41 0 3899 0 vsize: 15760 [startup+500.046 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3550 0 0 0 49989 19 0 0 25 0 1 0 490619640 16138240 3528 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3528 603 41 0 3899 0 vsize: 15760 [startup+510.047 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3550 0 0 0 50989 19 0 0 25 0 1 0 490619640 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3528 603 41 0 3899 0 vsize: 15760 [startup+520.046 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3550 0 0 0 51989 19 0 0 25 0 1 0 490619640 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3528 603 41 0 3899 0 vsize: 15760 [startup+530.047 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3551 0 0 0 52989 19 0 0 25 0 1 0 490619640 16138240 3529 4294967295 134512640 134672761 3221224544 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3529 603 41 0 3899 0 vsize: 15760 [startup+540.048 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3645 0 0 0 53989 19 0 0 25 0 1 0 490619640 16535552 3623 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4037 3623 603 41 0 3996 0 vsize: 16148 [startup+550.047 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3856 0 0 0 54989 20 0 0 25 0 1 0 490619640 17469440 3834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3834 603 41 0 4224 0 vsize: 17060 [startup+560.047 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3860 0 0 0 55989 20 0 0 25 0 1 0 490619640 17469440 3838 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3838 603 41 0 4224 0 vsize: 17060 [startup+570.048 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 56989 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+580.049 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 57989 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+590.049 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 58989 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+600.049 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 59989 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+610.049 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 60990 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+620.049 s] Raw data (loadavg): 1.00 0.99 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3862 0 0 0 61990 20 0 0 25 0 1 0 490619640 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3840 603 41 0 4224 0 vsize: 17060 [startup+630.05 s] Raw data (loadavg): 1.08 1.00 0.98 2/54 3117 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3867 0 0 0 62990 20 0 0 25 0 1 0 490619640 17469440 3845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4265 3845 603 41 0 4224 0 vsize: 17060 [startup+640.05 s] Raw data (loadavg): 1.07 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 63990 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223728 134558758 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+650.05 s] Raw data (loadavg): 1.06 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 64990 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+660.051 s] Raw data (loadavg): 1.05 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 65991 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+670.051 s] Raw data (loadavg): 1.04 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 66991 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223648 134560250 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+680.052 s] Raw data (loadavg): 1.03 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 67991 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+690.052 s] Raw data (loadavg): 1.03 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3900 0 0 0 68991 20 0 0 25 0 1 0 490619640 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4329 3878 603 41 0 4288 0 vsize: 17316 [startup+700.052 s] Raw data (loadavg): 1.02 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 69991 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+710.053 s] Raw data (loadavg): 1.02 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 70992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+720.053 s] Raw data (loadavg): 1.02 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 71992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+730.053 s] Raw data (loadavg): 1.01 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 72992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+740.053 s] Raw data (loadavg): 1.01 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 73992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+750.053 s] Raw data (loadavg): 1.01 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 74992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+760.053 s] Raw data (loadavg): 1.01 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 75992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+770.053 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 76992 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+780.054 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 77993 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+790.054 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 78993 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+800.054 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 79993 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+810.055 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 80993 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+820.056 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 81994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+830.057 s] Raw data (loadavg): 1.00 1.00 0.98 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 82994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+840.057 s] Raw data (loadavg): 1.08 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 83994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+850.057 s] Raw data (loadavg): 1.14 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 84994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+860.057 s] Raw data (loadavg): 1.12 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 85994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+870.057 s] Raw data (loadavg): 1.10 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 86994 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223708 134559748 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+880.057 s] Raw data (loadavg): 1.08 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 87995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+890.057 s] Raw data (loadavg): 1.07 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 88995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223636 134555596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+900.057 s] Raw data (loadavg): 1.06 1.03 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 89995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+910.057 s] Raw data (loadavg): 1.05 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 90995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+920.057 s] Raw data (loadavg): 1.04 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 91995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+930.058 s] Raw data (loadavg): 1.04 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 92995 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+940.058 s] Raw data (loadavg): 1.03 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 93996 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+950.058 s] Raw data (loadavg): 1.02 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 94996 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+960.059 s] Raw data (loadavg): 1.02 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 3979 0 0 0 95996 20 0 0 25 0 1 0 490619640 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3957 603 41 0 4352 0 vsize: 17572 [startup+970.059 s] Raw data (loadavg): 1.02 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4060 0 0 0 96996 20 0 0 25 0 1 0 490619640 18399232 4038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4038 603 41 0 4451 0 vsize: 17968 [startup+980.06 s] Raw data (loadavg): 1.01 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4060 0 0 0 97996 20 0 0 25 0 1 0 490619640 18399232 4038 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4038 603 41 0 4451 0 vsize: 17968 [startup+990.06 s] Raw data (loadavg): 1.01 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 98996 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1000.06 s] Raw data (loadavg): 1.01 1.02 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 99997 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1010.06 s] Raw data (loadavg): 1.01 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 100997 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1020.06 s] Raw data (loadavg): 1.01 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 101997 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1030.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 102997 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1040.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 103997 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1050.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 104998 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1060.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4068 0 0 0 105998 20 0 0 25 0 1 0 490619640 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1070.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4076 0 0 0 106998 20 0 0 25 0 1 0 490619640 18399232 4054 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4054 603 41 0 4451 0 vsize: 17968 [startup+1080.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4082 0 0 0 107998 20 0 0 25 0 1 0 490619640 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4528 4060 603 41 0 4487 0 vsize: 18112 [startup+1090.06 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4082 0 0 0 108999 20 0 0 25 0 1 0 490619640 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4528 4060 603 41 0 4487 0 vsize: 18112 [startup+1100.07 s] Raw data (loadavg): 1.00 1.01 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4082 0 0 0 109999 20 0 0 25 0 1 0 490619640 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4528 4060 603 41 0 4487 0 vsize: 18112 [startup+1110.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4082 0 0 0 111000 20 0 0 25 0 1 0 490619640 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4528 4060 603 41 0 4487 0 vsize: 18112 [startup+1120.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4126 0 0 0 112000 21 0 0 25 0 1 0 490619640 18677760 4104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4560 4104 603 41 0 4519 0 vsize: 18240 [startup+1130.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4130 0 0 0 113000 21 0 0 25 0 1 0 490619640 18677760 4108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4560 4108 603 41 0 4519 0 vsize: 18240 [startup+1140.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4145 0 0 0 113999 21 0 0 25 0 1 0 490619640 18677760 4123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4560 4123 603 41 0 4519 0 vsize: 18240 [startup+1150.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4246 0 0 0 114999 21 0 0 25 0 1 0 490619640 19206144 4224 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4689 4224 603 41 0 4648 0 vsize: 18756 [startup+1160.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4252 0 0 0 115999 22 0 0 25 0 1 0 490619640 19206144 4230 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4689 4230 603 41 0 4648 0 vsize: 18756 [startup+1170.07 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4270 0 0 0 116998 22 0 0 25 0 1 0 490619640 19361792 4248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4727 4248 603 41 0 4686 0 vsize: 18908 [startup+1180.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4271 0 0 0 117998 22 0 0 25 0 1 0 490619640 19361792 4249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4727 4249 603 41 0 4686 0 vsize: 18908 [startup+1190.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4283 0 0 0 118998 23 0 0 25 0 1 0 490619640 19361792 4261 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4727 4261 603 41 0 4686 0 vsize: 18908 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/54 3119 Raw data (stat): 3062 (minisat+) R 3061 24215 24214 0 -1 0 4285 0 0 0 119998 23 0 0 25 0 1 0 490619640 19361792 4263 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4727 4263 603 41 0 4686 0 vsize: 18908 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.09 s] Raw data (loadavg): 1.00 1.00 0.99 1/54 3119 Raw data (stat): 3062 (minisat+) Z 3061 24215 24214 0 -1 12 4288 0 0 0 119998 23 0 0 25 0 1 0 490619640 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.09 CPU time (s): 1200.23 CPU user time (s): 1199.99 CPU system time (s): 0.239963 CPU usage (%): 100.012 Max. virtual memory (Kb): 18908 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####