Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-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.02284 |
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 wulflinc20 THE 2005-04-21 02:37:43 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18704 boxname=wulflinc20 idbench=1439 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c361d02d5162bb0b133ab6ed38f9294 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0201.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0201.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-p0201.opb IDLAUNCH: 18704 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 681060 kB Buffers: 17284 kB Cached: 311920 kB SwapCached: 528 kB Active: 103724 kB Inactive: 227528 kB HighTotal: 131008 kB HighFree: 1344 kB LowTotal: 903652 kB LowFree: 679716 kB SwapTotal: 2097892 kB SwapFree: 2096468 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5112 kB Slab: 16544 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 02:57:46 (client local time) WITH STATUS 10 IN 1200.26 SECONDS stats: 18704 7 1200.26 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.84 0.94 0.91 2/54 27478 Raw data (stat): 27478 (runsolver) R 27477 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541535597 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.0007 s] Raw data (loadavg): 0.87 0.94 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 1629 0 0 0 994 3 0 0 25 0 1 0 541535597 8228864 1607 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2009 1607 603 41 0 1968 0 vsize: 8036 [startup+20.0003 s] Raw data (loadavg): 0.89 0.94 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 1988 0 0 0 1993 4 0 0 25 0 1 0 541535597 9850880 1966 4294967295 134512640 134672761 3221224544 3221223680 134560709 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.0011 s] Raw data (loadavg): 0.90 0.94 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 1988 0 0 0 2993 5 0 0 25 0 1 0 541535597 9850880 1966 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2405 1966 603 41 0 2364 0 vsize: 9620 [startup+40.0006 s] Raw data (loadavg): 0.92 0.94 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 2291 0 0 0 3992 5 0 0 25 0 1 0 541535597 11055104 2269 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2699 2269 603 41 0 2658 0 vsize: 10796 [startup+50.0014 s] Raw data (loadavg): 0.93 0.94 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 2455 0 0 0 4992 6 0 0 25 0 1 0 541535597 11730944 2433 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2864 2433 603 41 0 2823 0 vsize: 11456 [startup+60.0011 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3100 0 0 0 5990 8 0 0 25 0 1 0 541535597 14413824 3078 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3519 3078 603 41 0 3478 0 vsize: 14076 [startup+70.0443 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3100 0 0 0 6994 8 0 0 25 0 1 0 541535597 14413824 3078 4294967295 134512640 134672761 3221224544 3221223728 134558848 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3519 3078 603 41 0 3478 0 vsize: 14076 [startup+80.0635 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3101 0 0 0 7996 8 0 0 25 0 1 0 541535597 14401536 3079 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3079 603 41 0 3475 0 vsize: 14064 [startup+90.0632 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 8996 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+100.063 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 9997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+110.064 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 10997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+120.063 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 11997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+130.064 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 12997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+140.064 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 13996 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223704 134561029 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.065 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 14996 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223696 134559753 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+160.065 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 15996 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+170.064 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 16997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223728 134558629 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+180.065 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 17997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+190.065 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 18997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+200.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3102 0 0 0 19997 8 0 0 25 0 1 0 541535597 14401536 3080 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3516 3080 603 41 0 3475 0 vsize: 14064 [startup+210.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3315 0 0 0 20997 9 0 0 25 0 1 0 541535597 15204352 3293 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3712 3293 603 41 0 3671 0 vsize: 14848 [startup+220.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3320 0 0 0 21997 9 0 0 25 0 1 0 541535597 15204352 3298 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3712 3298 603 41 0 3671 0 vsize: 14848 [startup+230.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3332 0 0 0 22997 9 0 0 25 0 1 0 541535597 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3310 603 41 0 3704 0 vsize: 14980 [startup+240.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3332 0 0 0 23997 9 0 0 25 0 1 0 541535597 15339520 3310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3310 603 41 0 3704 0 vsize: 14980 [startup+250.066 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3333 0 0 0 24997 9 0 0 25 0 1 0 541535597 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+260.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3333 0 0 0 25997 9 0 0 25 0 1 0 541535597 15339520 3311 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+270.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3333 0 0 0 26997 9 0 0 25 0 1 0 541535597 15339520 3311 4294967295 134512640 134672761 3221224544 3221223648 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3311 603 41 0 3704 0 vsize: 14980 [startup+280.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 27997 9 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+290.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 28997 9 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3745 3312 603 41 0 3704 0 vsize: 14980 [startup+300.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 29998 9 0 0 25 0 1 0 541535597 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+310.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 30998 9 0 0 25 0 1 0 541535597 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+320.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 31998 9 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561190 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.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 32998 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 33998 10 0 0 25 0 1 0 541535597 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.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 34999 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223648 134560196 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.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 35999 10 0 0 25 0 1 0 541535597 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.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 36999 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 37999 10 0 0 25 0 1 0 541535597 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+390.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 38999 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560888 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.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 40000 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560996 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.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 41000 10 0 0 25 0 1 0 541535597 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+420.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 42000 10 0 0 25 0 1 0 541535597 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+430.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 43000 10 0 0 25 0 1 0 541535597 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.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 44000 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3334 0 0 0 45000 10 0 0 25 0 1 0 541535597 15339520 3312 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3450 0 0 0 46000 10 0 0 25 0 1 0 541535597 15736832 3428 4294967295 134512640 134672761 3221224544 3221223376 134565831 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.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3450 0 0 0 47000 10 0 0 25 0 1 0 541535597 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+480.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3549 0 0 0 48000 10 0 0 25 0 1 0 541535597 16138240 3527 4294967295 134512640 134672761 3221224544 3221223712 134561701 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.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3549 0 0 0 49001 10 0 0 25 0 1 0 541535597 16138240 3527 4294967295 134512640 134672761 3221224544 3221223712 134560876 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.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3550 0 0 0 50001 10 0 0 25 0 1 0 541535597 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3550 0 0 0 51001 10 0 0 25 0 1 0 541535597 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3550 0 0 0 52001 10 0 0 25 0 1 0 541535597 16138240 3528 4294967295 134512640 134672761 3221224544 3221223712 134560900 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.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3551 0 0 0 53001 10 0 0 25 0 1 0 541535597 16138240 3529 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3551 0 0 0 54001 10 0 0 25 0 1 0 541535597 16138240 3529 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3940 3529 603 41 0 3899 0 vsize: 15760 [startup+550.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3856 0 0 0 55001 12 0 0 25 0 1 0 541535597 17469440 3834 4294967295 134512640 134672761 3221224544 3221223712 134561193 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.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3860 0 0 0 56001 12 0 0 25 0 1 0 541535597 17469440 3838 4294967295 134512640 134672761 3221224544 3221223712 134561205 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.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 57001 12 0 0 25 0 1 0 541535597 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.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 58001 12 0 0 25 0 1 0 541535597 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+590.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 59001 12 0 0 25 0 1 0 541535597 17469440 3840 4294967295 134512640 134672761 3221224544 3221223712 134561190 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.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 60002 12 0 0 25 0 1 0 541535597 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+610.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 61002 12 0 0 25 0 1 0 541535597 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+620.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3862 0 0 0 62002 12 0 0 25 0 1 0 541535597 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.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3867 0 0 0 63002 12 0 0 25 0 1 0 541535597 17469440 3845 4294967295 134512640 134672761 3221224544 3221223712 134561167 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.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 64002 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560852 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.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 65002 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 66003 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 67003 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223680 134560675 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.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 68002 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134561133 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3900 0 0 0 69003 12 0 0 25 0 1 0 541535597 17731584 3878 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 70002 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134554662 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 71002 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223668 134566122 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 72003 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560855 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 73003 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560929 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.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 74003 12 0 0 25 0 1 0 541535597 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.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 75003 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134560906 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.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 76003 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134558843 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.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 77004 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223680 134565127 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.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 78004 12 0 0 25 0 1 0 541535597 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+790.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 79004 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223696 134561035 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 80004 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134558923 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.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 81004 12 0 0 25 0 1 0 541535597 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+820.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 82005 12 0 0 25 0 1 0 541535597 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+830.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 83005 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223636 1075351142 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 84005 12 0 0 25 0 1 0 541535597 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+850.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 85005 12 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223728 134559045 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.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 86005 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223704 134561240 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.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 87005 13 0 0 25 0 1 0 541535597 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+880.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 88006 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560313 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.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 89006 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560350 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 90006 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223680 134560706 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 91006 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223712 134561215 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.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 92006 13 0 0 25 0 1 0 541535597 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+930.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 93006 13 0 0 25 0 1 0 541535597 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 94007 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223648 134560184 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 95007 13 0 0 25 0 1 0 541535597 17993728 3957 4294967295 134512640 134672761 3221224544 3221223476 1074972064 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 96007 13 0 0 25 0 1 0 541535597 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.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 3979 0 0 0 97007 13 0 0 25 0 1 0 541535597 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+980.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4060 0 0 0 98007 13 0 0 25 0 1 0 541535597 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+990.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4064 0 0 0 99007 13 0 0 25 0 1 0 541535597 18399232 4042 4294967295 134512640 134672761 3221224544 3221223712 134560849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4042 603 41 0 4451 0 vsize: 17968 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 100007 13 0 0 25 0 1 0 541535597 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560871 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 101008 13 0 0 25 0 1 0 541535597 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 102008 13 0 0 25 0 1 0 541535597 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+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 103008 13 0 0 25 0 1 0 541535597 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 104008 13 0 0 25 0 1 0 541535597 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134561229 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 105008 13 0 0 25 0 1 0 541535597 18399232 4046 4294967295 134512640 134672761 3221224544 3221223500 1075349896 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 106009 13 0 0 25 0 1 0 541535597 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4068 0 0 0 107009 13 0 0 25 0 1 0 541535597 18399232 4046 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4046 603 41 0 4451 0 vsize: 17968 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4076 0 0 0 108009 13 0 0 25 0 1 0 541535597 18399232 4054 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4492 4054 603 41 0 4451 0 vsize: 17968 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4082 0 0 0 109009 13 0 0 25 0 1 0 541535597 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4082 0 0 0 110009 13 0 0 25 0 1 0 541535597 18546688 4060 4294967295 134512640 134672761 3221224544 3221223728 134558899 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4082 0 0 0 111009 13 0 0 25 0 1 0 541535597 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560937 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.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4082 0 0 0 112010 13 0 0 25 0 1 0 541535597 18546688 4060 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4528 4060 603 41 0 4487 0 vsize: 18112 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4126 0 0 0 113010 13 0 0 25 0 1 0 541535597 18677760 4104 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4560 4104 603 41 0 4519 0 vsize: 18240 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4130 0 0 0 114010 13 0 0 25 0 1 0 541535597 18677760 4108 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4560 4108 603 41 0 4519 0 vsize: 18240 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4141 0 0 0 115010 13 0 0 25 0 1 0 541535597 18677760 4119 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4560 4119 603 41 0 4519 0 vsize: 18240 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4246 0 0 0 116010 14 0 0 25 0 1 0 541535597 19206144 4224 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4689 4224 603 41 0 4648 0 vsize: 18756 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4252 0 0 0 117010 14 0 0 25 0 1 0 541535597 19206144 4230 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4689 4230 603 41 0 4648 0 vsize: 18756 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4269 0 0 0 118010 14 0 0 25 0 1 0 541535597 19361792 4247 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4727 4247 603 41 0 4686 0 vsize: 18908 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4271 0 0 0 119011 14 0 0 25 0 1 0 541535597 19361792 4249 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4727 4249 603 41 0 4686 0 vsize: 18908 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 27478 Raw data (stat): 27478 (minisat+) R 27477 27565 27564 0 -1 0 4283 0 0 0 120011 14 0 0 25 0 1 0 541535597 19361792 4261 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4727 4261 603 41 0 4686 0 vsize: 18908 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 27478 Raw data (stat): 27478 (minisat+) Z 27477 27565 27564 0 -1 12 4286 0 0 0 120011 14 0 0 25 0 1 0 541535597 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.1 CPU time (s): 1200.26 CPU user time (s): 1200.11 CPU system time (s): 0.149977 CPU usage (%): 100.014 Max. virtual memory (Kb): 18908 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####