Name | normalized-opb/submitted/een/normalized-p0201.opb |
MD5SUM | ff4eb45c2603a47e5b79b2649e926ba4 |
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.01984 |
Number of variables | 195 |
Total number of constraints | 133 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 26 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 3 |
Maximum length of a constraint | 65 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc23 THE 2005-04-14 21:25:48 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5160 boxname=wulflinc23 idbench=397 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ff4eb45c2603a47e5b79b2649e926ba4 /oldhome/oroussel/tmp/wulflinc23/normalized-p0201.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc23/normalized-p0201.opb /oldhome/oroussel/tmp/wulflinc23/normalized-p0201.opb IDLAUNCH: 5160 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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: 852576 kB Buffers: 35396 kB Cached: 104016 kB SwapCached: 192 kB Active: 63064 kB Inactive: 79348 kB HighTotal: 131008 kB HighFree: 23156 kB LowTotal: 903652 kB LowFree: 829420 kB SwapTotal: 2097136 kB SwapFree: 2096944 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6908 kB Slab: 34068 kB Committed_AS: 63472 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 21:45:50 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 5160 7 1200.22 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]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 134]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 3 c ---[ 132]---> BDD-cost: 3 c ---[ 131]---> BDD-cost: 3 c ---[ 130]---> BDD-cost: 3 c ---[ 129]---> BDD-cost: 3 c ---[ 128]---> BDD-cost: 11 c ---[ 127]---> BDD-cost: 11 c ---[ 126]---> BDD-cost: 11 c ---[ 125]---> BDD-cost: 11 c ---[ 124]---> BDD-cost: 11 c ---[ 123]---> BDD-cost: 11 c ---[ 122]---> BDD-cost: 11 c ---[ 121]---> BDD-cost: 11 c ---[ 120]---> BDD-cost: 11 c ---[ 119]---> BDD-cost: 11 c ---[ 118]---> BDD-cost: 11 c ---[ 117]---> BDD-cost: 11 c ---[ 116]---> BDD-cost: 11 c ---[ 115]---> BDD-cost: 11 c ---[ 114]---> BDD-cost: 11 c ---[ 113]---> BDD-cost: 11 c ---[ 112]---> BDD-cost: 11 c ---[ 111]---> BDD-cost: 11 c ---[ 110]---> BDD-cost: 11 c ---[ 109]---> BDD-cost: 11 c ---[ 108]---> BDD-cost: 11 c ---[ 107]---> BDD-cost: 11 c ---[ 106]---> BDD-cost: 11 c ---[ 105]---> BDD-cost: 11 c ---[ 104]---> BDD-cost: 11 c ---[ 103]---> BDD-cost: 11 c ---[ 102]---> BDD-cost: 11 c ---[ 101]---> BDD-cost: 11 c ---[ 100]---> BDD-cost: 11 c ---[ 99]---> BDD-cost: 11 c ---[ 98]---> BDD-cost: 11 c ---[ 97]---> BDD-cost: 11 c ---[ 96]---> BDD-cost: 11 c ---[ 95]---> BDD-cost: 11 c ---[ 94]---> BDD-cost: 11 c ---[ 93]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 11 c ---[ 91]---> BDD-cost: 11 c ---[ 90]---> BDD-cost: 11 c ---[ 89]---> BDD-cost: 11 c ---[ 88]---> BDD-cost: 11 c ---[ 87]---> BDD-cost: 11 c ---[ 86]---> BDD-cost: 11 c ---[ 85]---> BDD-cost: 11 c ---[ 84]---> BDD-cost: 11 c ---[ 83]---> BDD-cost: 11 c ---[ 82]---> BDD-cost: 11 c ---[ 81]---> BDD-cost: 11 c ---[ 80]---> BDD-cost: 11 c ---[ 79]---> BDD-cost: 11 c ---[ 78]---> BDD-cost: 11 c ---[ 77]---> BDD-cost: 11 c ---[ 76]---> BDD-cost: 11 c ---[ 75]---> BDD-cost: 11 c ---[ 74]---> BDD-cost: 11 c ---[ 72]---> BDD-cost: 13 c ---[ 70]---> BDD-cost: 15 c ---[ 68]---> BDD-cost: 15 c ---[ 66]---> BDD-cost: 13 c ---[ 64]---> BDD-cost: 13 c ---[ 62]---> BDD-cost: 13 c ---[ 60]---> BDD-cost: 13 c ---[ 58]---> BDD-cost: 13 c ---[ 56]---> BDD-cost: 13 c ---[ 54]---> BDD-cost: 13 c ---[ 52]---> BDD-cost: 13 c ---[ 50]---> BDD-cost: 13 c ---[ 48]---> BDD-cost: 13 c ---[ 46]---> BDD-cost: 13 c ---[ 44]---> BDD-cost: 13 c ---[ 42]---> BDD-cost: 13 c ---[ 40]---> BDD-cost: 13 c ---[ 38]---> BDD-cost: 13 c ---[ 36]---> BDD-cost: 13 c ---[ 31]---> BDD-cost: 39 c ---[ 28]---> BDD-cost: 54 c ---[ 27]---> BDD-cost: 42 c ---[ 26]---> BDD-cost: 42 c ---[ 25]---> BDD-cost: 73 c ---[ 24]---> BDD-cost: 73 c ---[ 23]---> BDD-cost: 98 c ---[ 22]---> BDD-cost: 160 c ---[ 21]---> BDD-cost: 85 c ---[ 20]---> BDD-cost: 85 c ---[ 19]---> BDD-cost: 201 c ---[ 18]---> BDD-cost: 107 c ---[ 17]---> BDD-cost: 107 c ---[ 16]---> BDD-cost: 241 c ---[ 15]---> BDD-cost: 128 c ---[ 14]---> BDD-cost: 128 c ---[ 13]---> BDD-cost: 150 c ---[ 12]---> BDD-cost: 150 c ---[ 11]---> BDD-cost: 281 c ---[ 10]---> BDD-cost: 321 c ---[ 9]---> BDD-cost: 172 c ---[ 8]---> BDD-cost: 172 c ---[ 7]---> BDD-cost: 194 c ---[ 6]---> BDD-cost: 194 c ---[ 5]---> BDD-cost: 361 c ---[ 4]---> BDD-cost: 1 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 1 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11741 34627 | 3913 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2321[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:21987 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22 | 60840 149261 | 20280 21 108 5.1 | 0.000 % | c | 122 | 60771 149095 | 22308 116 9072 78.2 | 0.586 % | c | 272 | 60333 148103 | 24538 263 10198 38.8 | 1.087 % | c ============================================================================== c [1mFound solution: 2304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 464 | 59190 145572 | 19730 360 10756 29.9 | 1.087 % | c | 564 | 56937 140394 | 21703 431 11589 26.9 | 6.067 % | c | 715 | 56667 139775 | 23873 579 15674 27.1 | 6.418 % | c | 940 | 56053 138362 | 26260 791 17405 22.0 | 7.522 % | c ============================================================================== c [1mFound solution: 2221[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 973 | 55214 136433 | 18404 810 17568 21.7 | 7.522 % | c | 1073 | 55078 136119 | 20244 909 31790 35.0 | 8.517 % | c | 1223 | 53987 133608 | 22268 1036 32305 31.2 | 9.937 % | c | 1452 | 53445 132352 | 24495 1232 40064 32.5 | 10.686 % | c ============================================================================== c [1mFound solution: 2166[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1536 | 52668 130555 | 17556 1307 41474 31.7 | 10.686 % | c | 1637 | 52668 130555 | 19311 1408 46677 33.2 | 11.681 % | c | 1787 | 52668 130555 | 21242 1558 51594 33.1 | 11.682 % | c ============================================================================== c [1mFound solution: 2136[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1825 | 52689 130614 | 17563 1596 52210 32.7 | 11.682 % | c | 1925 | 52689 130614 | 19319 1696 54746 32.3 | 11.679 % | c | 2080 | 52689 130614 | 21251 1851 60799 32.8 | 11.679 % | c ============================================================================== c [1mFound solution: 1963[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2126 | 52479 130144 | 17493 1888 62844 33.3 | 11.679 % | c | 2226 | 52479 130144 | 19242 1988 64360 32.4 | 12.091 % | c | 2377 | 52479 130144 | 21166 2139 70843 33.1 | 12.091 % | c ============================================================================== c [1mFound solution: 1959[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2471 | 52489 130172 | 17496 2233 72955 32.7 | 12.091 % | c | 2571 | 52322 129787 | 19245 2328 74840 32.1 | 12.323 % | c | 2721 | 51285 127390 | 21170 2429 80367 33.1 | 13.717 % | c | 2947 | 50170 124809 | 23287 2621 85422 32.6 | 15.200 % | c | 3287 | 48847 121747 | 25615 2911 101992 35.0 | 16.952 % | c | 3793 | 48358 120612 | 28177 3403 113615 33.4 | 17.588 % | c ============================================================================== c [1mFound solution: 1948[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4119 | 48366 120631 | 16122 3729 137025 36.7 | 17.588 % | c | 4219 | 48366 120631 | 17734 3829 138803 36.3 | 17.588 % | c | 4369 | 48048 119892 | 19507 3958 145830 36.8 | 18.022 % | c | 4594 | 46695 116764 | 21458 4091 147117 36.0 | 19.828 % | c | 4932 | 46689 116746 | 23604 4428 161011 36.4 | 19.837 % | c | 5439 | 46689 116746 | 25964 4935 174660 35.4 | 19.837 % | c ============================================================================== c [1mFound solution: 1939[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5595 | 46694 116758 | 15564 5091 183472 36.0 | 19.837 % | c | 5695 | 46694 116758 | 17120 5191 187041 36.0 | 19.838 % | c | 5846 | 46694 116758 | 18832 5342 193524 36.2 | 19.838 % | c | 6071 | 46694 116758 | 20715 5567 199369 35.8 | 19.838 % | c ============================================================================== c [1mFound solution: 1935[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6244 | 46756 116908 | 15585 5740 205127 35.7 | 19.838 % | c | 6346 | 46610 116564 | 17143 5837 209713 35.9 | 20.053 % | c | 6496 | 46529 116378 | 18857 5981 213413 35.7 | 20.158 % | c | 6721 | 46529 116378 | 20743 6206 228623 36.8 | 20.158 % | c ============================================================================== c [1mFound solution: 1931[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6870 | 44969 112759 | 14989 6212 230635 37.1 | 20.158 % | c | 6971 | 44969 112759 | 16487 6313 236280 37.4 | 22.294 % | c | 7121 | 44539 111755 | 18136 6433 238185 37.0 | 22.870 % | c | 7348 | 44147 110835 | 19950 6616 255984 38.7 | 23.437 % | c | 7687 | 44141 110817 | 21945 6953 266703 38.4 | 23.445 % | c | 8195 | 44132 110790 | 24139 7455 285481 38.3 | 23.458 % | c ============================================================================== c [1mFound solution: 1924[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8652 | 43344 108952 | 14448 7850 318221 40.5 | 23.458 % | c | 8753 | 43191 108593 | 15892 7939 320098 40.3 | 24.773 % | c | 8903 | 43162 108520 | 17482 8088 328118 40.6 | 24.824 % | c | 9130 | 43162 108520 | 19230 8315 335246 40.3 | 24.824 % | c ============================================================================== c [1mFound solution: 1914[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3291 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9281 | 45828 114675 | 15276 8466 342248 40.4 | 24.824 % | c | 9382 | 45828 114675 | 16803 8567 345184 40.3 | 23.183 % | c | 9532 | 45828 114675 | 18483 8717 356244 40.9 | 23.183 % | c | 9757 | 45828 114675 | 20332 8942 380246 42.5 | 23.183 % | c | 10096 | 45411 113705 | 22365 9242 389539 42.1 | 23.724 % | c | 10604 | 45101 112977 | 24602 9691 417766 43.1 | 24.120 % | c | 11364 | 45101 112977 | 27062 10451 459434 44.0 | 24.120 % | c ============================================================================== c [1mFound solution: 1909[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11707 | 44947 112614 | 14982 10785 486650 45.1 | 24.120 % | c | 11807 | 44926 112551 | 16480 10883 491738 45.2 | 24.394 % | c | 11958 | 44926 112551 | 18128 11034 493878 44.8 | 24.394 % | c | 12184 | 44926 112551 | 19941 11260 511699 45.4 | 24.394 % | c ============================================================================== c [1mFound solution: 1759[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12229 | 44945 112599 | 14981 11305 512517 45.3 | 24.394 % | c | 12332 | 44851 112382 | 16479 11400 515625 45.2 | 24.509 % | c | 12483 | 44851 112382 | 18127 11551 525382 45.5 | 24.509 % | c | 12708 | 44851 112382 | 19939 11776 530560 45.1 | 24.509 % | c | 13046 | 44847 112373 | 21933 12112 554374 45.8 | 24.513 % | c | 13553 | 44847 112373 | 24127 12619 586073 46.4 | 24.513 % | c | 14312 | 44395 111348 | 26539 13291 609205 45.8 | 25.144 % | c | 15452 | 44357 111261 | 29193 14408 672095 46.6 | 25.195 % | c | 17160 | 44357 111261 | 32113 16116 732967 45.5 | 25.195 % | c | 19724 | 44099 110658 | 35324 18624 917611 49.3 | 25.536 % | c | 23568 | 43596 109488 | 38856 22420 1217299 54.3 | 26.195 % | c ============================================================================== c [1mFound solution: 1748[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 27185 | 43512 109291 | 14504 26028 1445048 55.5 | 26.195 % | c | 27285 | 43512 109291 | 15954 13114 718324 54.8 | 26.347 % | c | 27435 | 43512 109291 | 17549 13264 723440 54.5 | 26.347 % | c | 27662 | 43512 109291 | 19304 13491 742053 55.0 | 26.347 % | c | 28001 | 43457 109164 | 21235 13826 756100 54.7 | 26.418 % | c | 28507 | 43457 109164 | 23358 14332 788988 55.1 | 26.418 % | c | 29266 | 43457 109164 | 25694 15091 851678 56.4 | 26.418 % | c | 30405 | 43457 109164 | 28264 16230 917258 56.5 | 26.418 % | c | 32116 | 43445 109128 | 31090 17939 1028851 57.4 | 26.433 % | c | 34678 | 43445 109128 | 34199 20501 1145720 55.9 | 26.433 % | c | 38524 | 43445 109128 | 37619 24347 1331202 54.7 | 26.433 % | c ============================================================================== c [1mFound solution: 1744[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 40084 | 43451 109141 | 14483 25907 1413810 54.6 | 26.433 % | c | 40184 | 43451 109141 | 15931 13054 485055 37.2 | 26.434 % | c | 40334 | 43451 109141 | 17524 13204 494401 37.4 | 26.434 % | c | 40560 | 43451 109141 | 19276 13430 510472 38.0 | 26.434 % | c | 40897 | 43451 109141 | 21204 13767 528771 38.4 | 26.434 % | c | 41405 | 43451 109141 | 23325 14275 562681 39.4 | 26.434 % | c | 42165 | 43451 109141 | 25657 15035 600347 39.9 | 26.434 % | c | 43307 | 43451 109141 | 28223 16177 663217 41.0 | 26.434 % | c | 45017 | 42985 108057 | 31045 17876 742191 41.5 | 27.022 % | c ============================================================================== c [1mFound solution: 1736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45161 | 42991 108073 | 14330 18020 750130 41.6 | 27.022 % | c | 45261 | 42991 108073 | 15763 18120 757033 41.8 | 27.022 % | c | 45412 | 42991 108073 | 17339 18271 763489 41.8 | 27.022 % | c | 45638 | 42991 108073 | 19073 18497 771489 41.7 | 27.022 % | c | 45975 | 42991 108073 | 20980 18834 791375 42.0 | 27.022 % | c | 46481 | 42987 108064 | 23078 19337 809336 41.9 | 27.026 % | c | 47240 | 42987 108064 | 25386 20096 863745 43.0 | 27.026 % | c | 48382 | 42987 108064 | 27925 21238 943746 44.4 | 27.026 % | c ============================================================================== c [1mFound solution: 1729[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 49754 | 42993 108079 | 14331 22610 1015698 44.9 | 27.026 % | c | 49859 | 42993 108079 | 15764 11410 419418 36.8 | 27.025 % | c | 50010 | 42993 108079 | 17340 11561 424641 36.7 | 27.025 % | c | 50235 | 42993 108079 | 19074 11786 438359 37.2 | 27.025 % | c | 50573 | 42993 108079 | 20982 12124 460647 38.0 | 27.025 % | c | 51079 | 42993 108079 | 23080 12630 483267 38.3 | 27.025 % | c | 51838 | 42993 108079 | 25388 13389 517484 38.6 | 27.025 % | c | 52980 | 42993 108079 | 27927 14531 578959 39.8 | 27.025 % | c | 54689 | 42993 108079 | 30719 16240 670254 41.3 | 27.025 % | c | 57253 | 42993 108079 | 33791 18804 805986 42.9 | 27.025 % | c | 61097 | 42993 108079 | 37170 22648 1043110 46.1 | 27.025 % | c | 66863 | 42984 108057 | 40888 28410 1338415 47.1 | 27.037 % | c | 75512 | 42921 107897 | 44976 37050 2118376 57.2 | 27.123 % | c ============================================================================== c [1mFound solution: 1721[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 86999 | 42811 107624 | 14270 48513 2865417 59.1 | 27.123 % | c | 87099 | 42811 107624 | 15697 18350 839087 45.7 | 27.265 % | c | 87249 | 42811 107624 | 17266 18500 845161 45.7 | 27.265 % | c ============================================================================== c [1mFound solution: 1716[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87420 | 42818 107641 | 14272 18671 852903 45.7 | 27.265 % | c | 87522 | 42818 107641 | 15699 18773 858915 45.8 | 27.263 % | c | 87673 | 42818 107641 | 17269 18924 867102 45.8 | 27.263 % | c ============================================================================== c [1mFound solution: 1709[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 87754 | 42824 107655 | 14274 19005 873644 46.0 | 27.263 % | c | 87854 | 42824 107655 | 15701 19105 878102 46.0 | 27.263 % | c | 88006 | 42824 107655 | 17271 19257 883087 45.9 | 27.263 % | c | 88231 | 42824 107655 | 18998 19482 899073 46.1 | 27.263 % | c | 88568 | 42824 107655 | 20898 19819 907472 45.8 | 27.263 % | c | 89074 | 42824 107655 | 22988 20325 927868 45.7 | 27.263 % | c | 89835 | 42824 107655 | 25287 21086 959351 45.5 | 27.263 % | c | 90975 | 42824 107655 | 27815 22226 1009265 45.4 | 27.263 % | c | 92683 | 42812 107619 | 30597 23931 1116385 46.7 | 27.279 % | c | 95247 | 42743 107460 | 33657 26491 1332738 50.3 | 27.365 % | c ============================================================================== c [1mFound solution: 1704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97966 | 42741 107458 | 14247 29207 1573586 53.9 | 27.365 % | c | 98067 | 42501 106900 | 15671 14695 680378 46.3 | 27.689 % | c | 98221 | 42501 106900 | 17238 14849 692647 46.6 | 27.689 % | c | 98446 | 42501 106900 | 18962 15074 711042 47.2 | 27.689 % | c | 98783 | 42501 106900 | 20859 15411 737707 47.9 | 27.689 % | c | 99289 | 42501 106900 | 22944 15917 771236 48.5 | 27.689 % | c | 100049 | 42395 106656 | 25239 16670 793350 47.6 | 27.823 % | c ============================================================================== c [1mFound solution: 1694[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 100789 | 42400 106668 | 14133 17410 820456 47.1 | 27.823 % | c | 100891 | 42316 106471 | 15546 17506 822128 47.0 | 27.941 % | c | 101041 | 42316 106471 | 17100 17656 830622 47.0 | 27.941 % | c | 101266 | 42316 106471 | 18811 17881 833523 46.6 | 27.941 % | c | 101603 | 42296 106424 | 20692 18216 854152 46.9 | 27.968 % | c | 102109 | 42296 106424 | 22761 18722 881251 47.1 | 27.968 % | c | 102869 | 42296 106424 | 25037 19482 923636 47.4 | 27.968 % | c | 104008 | 42296 106424 | 27541 20621 1002974 48.6 | 27.968 % | c | 105717 | 42201 106203 | 30295 22325 1112136 49.8 | 28.094 % | c ============================================================================== c [1mFound solution: 1691[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 106698 | 42206 106214 | 14068 23306 1194126 51.2 | 28.094 % | c | 106800 | 42206 106214 | 15474 11755 439579 37.4 | 28.094 % | c | 106951 | 41960 105641 | 17022 11888 442183 37.2 | 28.419 % | c | 107176 | 41960 105641 | 18724 12113 454948 37.6 | 28.419 % | c | 107513 | 41960 105641 | 20596 12450 472512 38.0 | 28.419 % | c ============================================================================== c [1mFound solution: 1684[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107802 | 41965 105652 | 13988 12739 489211 38.4 | 28.419 % | c | 107902 | 41965 105652 | 15386 12839 496709 38.7 | 28.419 % | c | 108054 | 41959 105640 | 16925 12989 500059 38.5 | 28.427 % | c | 108283 | 41794 105269 | 18618 12922 495216 38.3 | 28.635 % | c | 108621 | 41735 105135 | 20479 13241 500692 37.8 | 28.705 % | c | 109127 | 41732 105126 | 22527 13746 535569 39.0 | 28.709 % | c | 109886 | 41732 105126 | 24780 14505 561412 38.7 | 28.709 % | c | 111025 | 41726 105108 | 27258 15643 673525 43.1 | 28.717 % | c | 112734 | 41102 103658 | 29984 17271 759767 44.0 | 29.546 % | c ============================================================================== c [1mFound solution: 1667[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112862 | 41147 103764 | 13715 17399 768153 44.1 | 29.546 % | c | 112962 | 41147 103764 | 15086 17499 771190 44.1 | 29.533 % | c | 113112 | 41147 103764 | 16595 17649 775472 43.9 | 29.533 % | c | 113338 | 41147 103764 | 18254 17875 782287 43.8 | 29.533 % | c | 113676 | 41125 103714 | 20080 18207 795126 43.7 | 29.564 % | c | 114182 | 41125 103714 | 22088 18713 822570 44.0 | 29.564 % | c | 114943 | 41125 103714 | 24296 19474 860623 44.2 | 29.564 % | c | 116083 | 41125 103714 | 26726 20614 921723 44.7 | 29.564 % | c ============================================================================== c [1mFound solution: 1663[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 117182 | 41130 103725 | 13710 21713 983432 45.3 | 29.564 % | c | 117283 | 41130 103725 | 15081 10958 348621 31.8 | 29.566 % | c | 117434 | 41130 103725 | 16589 11109 350539 31.6 | 29.566 % | c | 117659 | 41130 103725 | 18248 11334 357808 31.6 | 29.566 % | c | 117996 | 40870 103125 | 20072 11654 367895 31.6 | 29.882 % | c | 118502 | 40870 103125 | 22080 12160 387551 31.9 | 29.882 % | c | 119261 | 40870 103125 | 24288 12919 408418 31.6 | 29.882 % | c ============================================================================== c [1mFound solution: 1661[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 119511 | 40884 103161 | 13628 13169 421521 32.0 | 29.882 % | c | 119614 | 40741 102828 | 14990 13263 423078 31.9 | 30.071 % | c | 119764 | 40741 102828 | 16489 13413 428871 32.0 | 30.071 % | c | 119990 | 40741 102828 | 18138 13639 440457 32.3 | 30.071 % | c | 120329 | 40741 102828 | 19952 13978 459794 32.9 | 30.071 % | c | 120835 | 40741 102828 | 21948 14484 478929 33.1 | 30.071 % | c | 121595 | 40741 102828 | 24142 15244 512143 33.6 | 30.071 % | c | 122736 | 40741 102828 | 26557 16385 573126 35.0 | 30.071 % | c | 124444 | 40741 102828 | 29212 18093 664548 36.7 | 30.071 % | c | 127008 | 40741 102828 | 32134 20657 777134 37.6 | 30.071 % | c ============================================================================== c [1mFound solution: 1656[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 130089 | 40745 102841 | 13581 23738 899116 37.9 | 30.071 % | c | 130192 | 40745 102841 | 14939 11972 322953 27.0 | 30.071 % | c | 130342 | 40745 102841 | 16433 12122 329170 27.2 | 30.071 % | c | 130567 | 40745 102841 | 18076 12347 333628 27.0 | 30.072 % | c | 130904 | 40745 102841 | 19883 12684 346118 27.3 | 30.072 % | c | 131412 | 40745 102841 | 21872 13192 369164 28.0 | 30.072 % | c | 132173 | 40745 102841 | 24059 13953 409035 29.3 | 30.071 % | c | 133313 | 40725 102794 | 26465 15088 439980 29.2 | 30.099 % | c | 135021 | 40715 102768 | 29112 16793 516035 30.7 | 30.114 % | c ============================================================================== c [1mFound solution: 1652[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 135571 | 40722 102793 | 13574 17343 537198 31.0 | 30.114 % | c | 135673 | 40722 102793 | 14931 17445 543058 31.1 | 30.112 % | c | 135824 | 40722 102793 | 16424 17596 547935 31.1 | 30.112 % | c | 136051 | 40722 102793 | 18066 17823 558959 31.4 | 30.112 % | c | 136388 | 40722 102793 | 19873 18160 570744 31.4 | 30.112 % | c | 136900 | 40722 102793 | 21861 18672 606492 32.5 | 30.113 % | c | 137659 | 40722 102793 | 24047 19431 650239 33.5 | 30.112 % | c | 138801 | 40722 102793 | 26451 20573 705072 34.3 | 30.112 % | c | 140509 | 40722 102793 | 29097 22281 792761 35.6 | 30.112 % | c ============================================================================== c [1mFound solution: 1651[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 142457 | 40716 102777 | 13572 24224 905816 37.4 | 30.112 % | c | 142557 | 40716 102777 | 14929 12212 387737 31.8 | 30.128 % | c | 142707 | 40716 102777 | 16422 12362 392691 31.8 | 30.128 % | c | 142933 | 40716 102777 | 18064 12588 399321 31.7 | 30.128 % | c | 143270 | 40716 102777 | 19870 12925 415415 32.1 | 30.128 % | c | 143776 | 40716 102777 | 21857 13431 436400 32.5 | 30.128 % | c | 144537 | 40716 102777 | 24043 14192 469687 33.1 | 30.128 % | c | 145676 | 40716 102777 | 26447 15331 521292 34.0 | 30.128 % | c ============================================================================== c [1mFound solution: 1644[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 146892 | 40720 102787 | 13573 16547 575446 34.8 | 30.128 % | c | 146995 | 40720 102787 | 14930 16650 581097 34.9 | 30.129 % | c | 147146 | 40720 102787 | 16423 16801 582869 34.7 | 30.129 % | c | 147371 | 40720 102787 | 18065 17026 591875 34.8 | 30.129 % | c | 147712 | 40720 102787 | 19872 17367 600578 34.6 | 30.129 % | c | 148219 | 40720 102787 | 21859 17874 617502 34.5 | 30.129 % | c | 148978 | 40720 102787 | 24045 18633 648881 34.8 | 30.129 % | c | 150117 | 40720 102787 | 26449 19772 710266 35.9 | 30.129 % | c | 151825 | 40720 102787 | 29094 21480 785614 36.6 | 30.129 % | c | 154387 | 40720 102787 | 32004 24042 880535 36.6 | 30.129 % | c ============================================================================== c [1mFound solution: 1642[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 154777 | 40726 102802 | 13575 24432 906188 37.1 | 30.129 % | c | 154877 | 40726 102802 | 14932 12316 335227 27.2 | 30.128 % | c | 155027 | 40726 102802 | 16425 12466 342339 27.5 | 30.128 % | c | 155252 | 40726 102802 | 18068 12691 355758 28.0 | 30.128 % | c | 155590 | 40726 102802 | 19875 13029 368814 28.3 | 30.128 % | c | 156099 | 40726 102802 | 21862 13538 389774 28.8 | 30.128 % | c | 156858 | 40726 102802 | 24048 14297 425274 29.7 | 30.128 % | c | 157997 | 40726 102802 | 26453 15436 460574 29.8 | 30.128 % | c | 159706 | 40726 102802 | 29099 17145 510125 29.8 | 30.128 % | c | 162272 | 40726 102802 | 32009 19711 608934 30.9 | 30.128 % | c | 166116 | 40726 102802 | 35210 23555 759486 32.2 | 30.128 % | c | 171882 | 40726 102802 | 38731 29321 1114603 38.0 | 30.128 % | c | 180531 | 40726 102802 | 42604 37970 1447309 38.1 | 30.128 % | c | 193506 | 40711 102757 | 46864 50940 2113661 41.5 | 30.148 % | c ============================================================================== c [1mFound solution: 1639[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 195154 | 40714 102764 | 13571 52588 2224442 42.3 | 30.148 % | c | 195255 | 40714 102764 | 14928 19845 732694 36.9 | 30.149 % | c | 195408 | 40714 102764 | 16420 19998 741441 37.1 | 30.149 % | c ============================================================================== c [1mFound solution: 1631[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 4 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 195571 | 40720 102778 | 13573 20161 748582 37.1 | 30.149 % | c | 195671 | 40720 102778 | 14930 20261 750087 37.0 | 30.148 % | c | 195821 | 40714 102764 | 16423 20408 752993 36.9 | 30.156 % | c | 196047 | 40714 102764 | 18065 20634 763296 37.0 | 30.156 % | c | 196384 | 40714 102764 | 19872 20971 786775 37.5 | 30.156 % | c | 196892 | 40714 102764 | 21859 21479 819658 38.2 | 30.156 % | c | 197652 | 40708 102746 | 24045 22238 864204 38.9 | 30.164 % | c | 198792 | 40708 102746 | 26449 23378 920169 39.4 | 30.164 % | c | 200501 | 40708 102746 | 29094 25087 1032119 41.1 | 30.164 % | c | 203063 | 40708 102746 | 32004 27649 1212199 43.8 | 30.164 % | c | 206908 | 40708 102746 | 35204 31494 1422349 45.2 | 30.164 % | c | 212675 | 40708 102746 | 38725 37261 1761049 47.3 | 30.164 % | c | 221324 | 40708 102746 | 42597 45910 2183773 47.6 | 30.164 % | c | 234298 | 40652 102615 | 46857 25366 975711 38.5 | 30.234 % | c ============================================================================== c [1mFound solution: 1623[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 5 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 248606 | 40658 102629 | 13552 39674 2053944 51.8 | 30.234 % | c | 248706 | 40516 102298 | 14907 16548 1008096 60.9 | 30.421 % | c | 248858 | 40516 102298 | 16397 16700 1013335 60.7 | 30.421 % | c | 249083 | 40513 102289 | 18037 16923 1023539 60.5 | 30.424 % | c | 249421 | 40513 102289 | 19841 17261 1032090 59.8 | 30.424 % | c | 249928 | 40513 102289 | 21825 17768 1050100 59.1 | 30.424 % | c | 250689 | 40513 102289 | 24008 18529 1075792 58.1 | 30.424 % | c | 251829 | 40513 102289 | 26409 19669 1120189 57.0 | 30.424 % | c | 253537 | 40352 101910 | 29049 21357 1252590 58.7 | 30.647 % | c | 256100 | 40352 101910 | 31954 23920 1396669 58.4 | 30.647 % | c | 259945 | 40352 101910 | 35150 27765 1641354 59.1 | 30.647 % | c | 265711 | 40352 101910 | 38665 33531 1958634 58.4 | 30.647 % | c | 274360 | 40352 101910 | 42531 42180 2471283 58.6 | 30.647 % | #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.93 0.97 0.91 2/54 13249 Raw data (stat): 13249 (runsolver) R 13248 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487816370 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 2391 0 0 0 993 6 0 0 25 0 1 0 487816370 11665408 2318 4294967295 134512640 134672761 3221224560 3221223664 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2848 2318 603 41 0 2807 0 vsize: 11392 [startup+20.0014 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 2527 0 0 0 1991 6 0 0 25 0 1 0 487816370 12312576 2454 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3006 2454 603 41 0 2965 0 vsize: 12024 [startup+30.0011 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 2806 0 0 0 2990 7 0 0 25 0 1 0 487816370 13250560 2733 4294967295 134512640 134672761 3221224560 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3235 2733 603 41 0 3194 0 vsize: 12940 [startup+40.0014 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 3002 0 0 0 3990 8 0 0 25 0 1 0 487816370 14053376 2929 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3431 2929 603 41 0 3390 0 vsize: 13724 [startup+50.0014 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 3191 0 0 0 4989 9 0 0 25 0 1 0 487816370 14852096 3118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3626 3118 603 41 0 3585 0 vsize: 14504 [startup+60.0021 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 3399 0 0 0 5989 9 0 0 25 0 1 0 487816370 15691776 3326 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3831 3326 603 41 0 3790 0 vsize: 15324 [startup+70.0024 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 3655 0 0 0 6987 11 0 0 25 0 1 0 487816370 16752640 3582 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4090 3582 603 41 0 4049 0 vsize: 16360 [startup+80.0083 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 3873 0 0 0 7988 11 0 0 25 0 1 0 487816370 17682432 3800 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4317 3800 603 41 0 4276 0 vsize: 17268 [startup+90.0089 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4025 0 0 0 8987 12 0 0 25 0 1 0 487816370 18210816 3952 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4446 3952 603 41 0 4405 0 vsize: 17784 [startup+100.008 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4025 0 0 0 9988 12 0 0 25 0 1 0 487816370 18210816 3952 4294967295 134512640 134672761 3221224560 3221223664 134560267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4446 3952 603 41 0 4405 0 vsize: 17784 [startup+110.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4025 0 0 0 10988 12 0 0 25 0 1 0 487816370 18210816 3952 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4446 3952 603 41 0 4405 0 vsize: 17784 [startup+120.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4025 0 0 0 11988 12 0 0 25 0 1 0 487816370 18210816 3952 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4446 3952 603 41 0 4405 0 vsize: 17784 [startup+130.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4025 0 0 0 12988 12 0 0 25 0 1 0 487816370 18210816 3952 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4446 3952 603 41 0 4405 0 vsize: 17784 [startup+140.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4066 0 0 0 13988 12 0 0 25 0 1 0 487816370 18468864 3993 4294967295 134512640 134672761 3221224560 3221223728 134560885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 3993 603 41 0 4468 0 vsize: 18036 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4066 0 0 0 14988 12 0 0 25 0 1 0 487816370 18468864 3993 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 3993 603 41 0 4468 0 vsize: 18036 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4066 0 0 0 15989 12 0 0 25 0 1 0 487816370 18468864 3993 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 3993 603 41 0 4468 0 vsize: 18036 [startup+170.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4066 0 0 0 16989 12 0 0 25 0 1 0 487816370 18468864 3993 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 3993 603 41 0 4468 0 vsize: 18036 [startup+180.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 17989 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223120 134597188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+190.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 18989 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 19989 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+210.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 20990 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223664 134560313 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+220.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 21990 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4078 0 0 0 22990 12 0 0 25 0 1 0 487816370 18468864 4005 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4005 603 41 0 4468 0 vsize: 18036 [startup+240.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4079 0 0 0 23990 12 0 0 25 0 1 0 487816370 18468864 4006 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4509 4006 603 41 0 4468 0 vsize: 18036 [startup+250.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4119 0 0 0 24990 12 0 0 25 0 1 0 487816370 18599936 4046 4294967295 134512640 134672761 3221224560 3221223664 134560412 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4541 4046 603 41 0 4500 0 vsize: 18164 [startup+260.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4318 0 0 0 25991 13 0 0 25 0 1 0 487816370 19529728 4245 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4768 4245 603 41 0 4727 0 vsize: 19072 [startup+270.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4542 0 0 0 26990 13 0 0 25 0 1 0 487816370 20447232 4469 4294967295 134512640 134672761 3221224560 3221223744 134559318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4992 4469 603 41 0 4951 0 vsize: 19968 [startup+280.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4763 0 0 0 27989 14 0 0 25 0 1 0 487816370 21385216 4690 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5221 4690 603 41 0 5180 0 vsize: 20884 [startup+290.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 4967 0 0 0 28989 15 0 0 25 0 1 0 487816370 22188032 4894 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5417 4894 603 41 0 5376 0 vsize: 21668 [startup+300.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5149 0 0 0 29989 15 0 0 25 0 1 0 487816370 23003136 5076 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5616 5076 603 41 0 5575 0 vsize: 22464 [startup+310.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5300 0 0 0 30988 16 0 0 25 0 1 0 487816370 23539712 5227 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5747 5227 603 41 0 5706 0 vsize: 22988 [startup+320.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5419 0 0 0 31988 16 0 0 25 0 1 0 487816370 24068096 5346 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5876 5346 603 41 0 5835 0 vsize: 23504 [startup+330.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5535 0 0 0 32987 17 0 0 25 0 1 0 487816370 24596480 5462 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6005 5462 603 41 0 5964 0 vsize: 24020 [startup+340.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5680 0 0 0 33988 17 0 0 25 0 1 0 487816370 25124864 5607 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6134 5607 603 41 0 6093 0 vsize: 24536 [startup+350.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 34987 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223696 134560652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+360.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 35987 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+370.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 36987 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+380.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 37988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+390.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 38988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+400.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 39988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+410.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 40988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+420.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 41988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+430.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 42988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+440.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 43988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+450.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 44988 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+460.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5775 0 0 0 45989 18 0 0 25 0 1 0 487816370 25522176 5702 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5702 603 41 0 6190 0 vsize: 24924 [startup+470.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5777 0 0 0 46989 18 0 0 25 0 1 0 487816370 25522176 5704 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5704 603 41 0 6190 0 vsize: 24924 [startup+480.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5777 0 0 0 47989 18 0 0 25 0 1 0 487816370 25522176 5704 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5704 603 41 0 6190 0 vsize: 24924 [startup+490.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5777 0 0 0 48989 18 0 0 25 0 1 0 487816370 25522176 5704 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5704 603 41 0 6190 0 vsize: 24924 [startup+500.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5777 0 0 0 49989 18 0 0 25 0 1 0 487816370 25522176 5704 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5704 603 41 0 6190 0 vsize: 24924 [startup+510.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 50989 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223664 134554673 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+520.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 51989 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223664 134560191 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+530.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 52990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+540.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 53990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223664 134560250 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+550.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 54990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+560.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 55990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+570.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 56990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+580.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 57990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+590.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 58990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+600.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5778 0 0 0 59990 19 0 0 25 0 1 0 487816370 25522176 5705 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5705 603 41 0 6190 0 vsize: 24924 [startup+610.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5779 0 0 0 60991 19 0 0 25 0 1 0 487816370 25522176 5706 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5706 603 41 0 6190 0 vsize: 24924 [startup+620.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5779 0 0 0 61991 19 0 0 25 0 1 0 487816370 25522176 5706 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5706 603 41 0 6190 0 vsize: 24924 [startup+630.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5779 0 0 0 62991 19 0 0 25 0 1 0 487816370 25522176 5706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5706 603 41 0 6190 0 vsize: 24924 [startup+640.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5779 0 0 0 63991 19 0 0 25 0 1 0 487816370 25522176 5706 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5706 603 41 0 6190 0 vsize: 24924 [startup+650.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 64991 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+660.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 65991 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+670.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 66991 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+680.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 67992 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223664 134560276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+690.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 68992 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+700.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5780 0 0 0 69992 19 0 0 25 0 1 0 487816370 25522176 5707 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5707 603 41 0 6190 0 vsize: 24924 [startup+710.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5781 0 0 0 70992 19 0 0 25 0 1 0 487816370 25522176 5708 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5708 603 41 0 6190 0 vsize: 24924 [startup+720.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5781 0 0 0 71992 19 0 0 25 0 1 0 487816370 25522176 5708 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5708 603 41 0 6190 0 vsize: 24924 [startup+730.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5781 0 0 0 72993 19 0 0 25 0 1 0 487816370 25522176 5708 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5708 603 41 0 6190 0 vsize: 24924 [startup+740.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5781 0 0 0 73993 20 0 0 25 0 1 0 487816370 25522176 5708 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5708 603 41 0 6190 0 vsize: 24924 [startup+750.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5784 0 0 0 74993 20 0 0 25 0 1 0 487816370 25522176 5711 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5711 603 41 0 6190 0 vsize: 24924 [startup+760.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5784 0 0 0 75993 20 0 0 25 0 1 0 487816370 25522176 5711 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5711 603 41 0 6190 0 vsize: 24924 [startup+770.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5785 0 0 0 76993 20 0 0 25 0 1 0 487816370 25522176 5712 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5712 603 41 0 6190 0 vsize: 24924 [startup+780.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5787 0 0 0 77993 20 0 0 25 0 1 0 487816370 25522176 5714 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5714 603 41 0 6190 0 vsize: 24924 [startup+790.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 78993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+800.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 79993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223696 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+810.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 80993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+820.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 81993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+830.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 82993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+840.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 83993 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+850.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 84994 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+860.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 85994 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+870.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 86994 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+880.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 87994 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+890.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 88994 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+900.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 89995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+910.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 90995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+920.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 91995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+930.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 92995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+940.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 93995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+950.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 94995 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+960.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 95996 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+970.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 96996 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+980.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 97996 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+990.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 98996 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 99996 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 100997 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 101997 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 102997 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 103997 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 104997 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 105998 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 106998 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 107998 20 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 108998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223684 134566077 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 109998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 110998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 111998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 112998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 113998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 114998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5789 0 0 0 115998 21 0 0 25 0 1 0 487816370 25522176 5716 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6231 5716 603 41 0 6190 0 vsize: 24924 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5855 0 0 0 116998 21 0 0 25 0 1 0 487816370 25784320 5782 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6295 5782 603 41 0 6254 0 vsize: 25180 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 5983 0 0 0 117998 22 0 0 25 0 1 0 487816370 26324992 5910 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6427 5910 603 41 0 6386 0 vsize: 25708 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 6112 0 0 0 118998 22 0 0 25 0 1 0 487816370 26857472 6039 4294967295 134512640 134672761 3221224560 3221223664 134560005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6557 6039 603 41 0 6516 0 vsize: 26228 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 13249 Raw data (stat): 13249 (minisat+) R 13248 3260 3259 0 -1 0 6212 0 0 0 119997 22 0 0 25 0 1 0 487816370 27254784 6139 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6654 6139 603 41 0 6613 0 vsize: 26616 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 13249 Raw data (stat): 13249 (minisat+) Z 13248 3260 3259 0 -1 12 6215 0 0 0 119997 23 0 0 25 0 1 0 487816370 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.05 CPU time (s): 1200.22 CPU user time (s): 1199.98 CPU system time (s): 0.239963 CPU usage (%): 100.014 Max. virtual memory (Kb): 26616 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####