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 wulflinc8 THE 2005-04-14 21:19:01 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=5153 boxname=wulflinc8 idbench=397 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: ff4eb45c2603a47e5b79b2649e926ba4 /oldhome/oroussel/tmp/wulflinc8/normalized-p0201.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc8/normalized-p0201.opb IDLAUNCH: 5153 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 858908 kB Buffers: 38024 kB Cached: 115860 kB SwapCached: 0 kB Active: 82944 kB Inactive: 75616 kB HighTotal: 131008 kB HighFree: 9464 kB LowTotal: 903652 kB LowFree: 849444 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6932 kB Slab: 11584 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 21:39:04 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 5153 7 1200.18 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 % | c | 287334 | 40342 101886 | 46785 21232 859949 40.5 | 30.662 % | #### 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.85 0.94 0.90 2/54 5985 Raw data (stat): 5985 (runsolver) R 5984 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 415990886 1052672 99 4294967295 134512640 135381576 3221224544 3221219788 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+9.99986 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 2409 0 0 0 991 7 0 0 25 0 1 0 415990886 11706368 2336 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2858 2336 603 41 0 2817 0 vsize: 11432 [startup+20.0005 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 2575 0 0 0 1990 7 0 0 25 0 1 0 415990886 12402688 2502 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3028 2502 603 41 0 2987 0 vsize: 12112 [startup+30.0008 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 2826 0 0 0 2989 8 0 0 25 0 1 0 415990886 13307904 2753 4294967295 134512640 134672761 3221224640 3221223808 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3249 2753 603 41 0 3208 0 vsize: 12996 [startup+40.002 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 3043 0 0 0 3987 9 0 0 25 0 1 0 415990886 14221312 2970 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3472 2970 603 41 0 3431 0 vsize: 13888 [startup+50.0018 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 3228 0 0 0 4987 10 0 0 25 0 1 0 415990886 14884864 3155 4294967295 134512640 134672761 3221224640 3221223808 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3634 3155 603 41 0 3593 0 vsize: 14536 [startup+60.0018 s] Raw data (loadavg): 0.94 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 3461 0 0 0 5986 10 0 0 25 0 1 0 415990886 16003072 3388 4294967295 134512640 134672761 3221224640 3221223744 134560010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3907 3388 603 41 0 3866 0 vsize: 15628 [startup+70.0024 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 3736 0 0 0 6986 11 0 0 25 0 1 0 415990886 17063936 3663 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4166 3663 603 41 0 4125 0 vsize: 16664 [startup+80.0021 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 3950 0 0 0 7985 12 0 0 25 0 1 0 415990886 17993728 3877 4294967295 134512640 134672761 3221224640 3221223808 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4393 3877 603 41 0 4352 0 vsize: 17572 [startup+90.0032 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4063 0 0 0 8985 12 0 0 25 0 1 0 415990886 18341888 3990 4294967295 134512640 134672761 3221224640 3221223800 134561238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4478 3990 603 41 0 4437 0 vsize: 17912 [startup+100.003 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4063 0 0 0 9985 12 0 0 25 0 1 0 415990886 18341888 3990 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4478 3990 603 41 0 4437 0 vsize: 17912 [startup+110.002 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4063 0 0 0 10984 12 0 0 25 0 1 0 415990886 18341888 3990 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4478 3990 603 41 0 4437 0 vsize: 17912 [startup+120.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4063 0 0 0 11984 12 0 0 25 0 1 0 415990886 18341888 3990 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4478 3990 603 41 0 4437 0 vsize: 17912 [startup+130.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4063 0 0 0 12984 13 0 0 25 0 1 0 415990886 18341888 3990 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4478 3990 603 41 0 4437 0 vsize: 17912 [startup+140.003 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4105 0 0 0 13984 13 0 0 25 0 1 0 415990886 18513920 4032 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 4032 603 41 0 4479 0 vsize: 18080 [startup+150.004 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4105 0 0 0 14984 13 0 0 25 0 1 0 415990886 18513920 4032 4294967295 134512640 134672761 3221224640 3221223808 134561201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 4032 603 41 0 4479 0 vsize: 18080 [startup+160.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4105 0 0 0 15984 13 0 0 25 0 1 0 415990886 18513920 4032 4294967295 134512640 134672761 3221224640 3221223776 134560619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 4032 603 41 0 4479 0 vsize: 18080 [startup+170.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4105 0 0 0 16984 13 0 0 25 0 1 0 415990886 18513920 4032 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4520 4032 603 41 0 4479 0 vsize: 18080 [startup+180.004 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 17984 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+190.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 18985 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+200.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 19985 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+210.005 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 20985 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+220.006 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 21985 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+230.006 s] Raw data (loadavg): 0.99 0.96 0.91 3/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4117 0 0 0 22985 13 0 0 25 0 1 0 415990886 18612224 4044 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4544 4044 603 41 0 4503 0 vsize: 18176 [startup+240.007 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4153 0 0 0 23986 13 0 0 25 0 1 0 415990886 18743296 4080 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4576 4080 603 41 0 4535 0 vsize: 18304 [startup+250.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4366 0 0 0 24985 14 0 0 25 0 1 0 415990886 19668992 4293 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4802 4293 603 41 0 4761 0 vsize: 19208 [startup+260.008 s] Raw data (loadavg): 0.99 0.97 0.91 3/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4591 0 0 0 25985 14 0 0 25 0 1 0 415990886 20594688 4518 4294967295 134512640 134672761 3221224640 3221223744 134559905 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5028 4518 603 41 0 4987 0 vsize: 20112 [startup+270.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 4832 0 0 0 26984 15 0 0 25 0 1 0 415990886 21663744 4759 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5289 4759 603 41 0 5248 0 vsize: 21156 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5028 0 0 0 27983 16 0 0 25 0 1 0 415990886 22466560 4955 4294967295 134512640 134672761 3221224640 3221223808 134560855 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5485 4955 603 41 0 5444 0 vsize: 21940 [startup+290.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5230 0 0 0 28983 17 0 0 25 0 1 0 415990886 23257088 5157 4294967295 134512640 134672761 3221224640 3221223744 134560376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5678 5157 603 41 0 5637 0 vsize: 22712 [startup+300.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5366 0 0 0 29983 17 0 0 25 0 1 0 415990886 23785472 5293 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5807 5293 603 41 0 5766 0 vsize: 23228 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5486 0 0 0 30983 18 0 0 25 0 1 0 415990886 24317952 5413 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5937 5413 603 41 0 5896 0 vsize: 23748 [startup+320.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5625 0 0 0 31982 18 0 0 25 0 1 0 415990886 24850432 5552 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6067 5552 603 41 0 6026 0 vsize: 24268 [startup+330.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5782 0 0 0 32982 19 0 0 25 0 1 0 415990886 25513984 5709 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6229 5709 603 41 0 6188 0 vsize: 24916 [startup+340.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 33982 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134561234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+350.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 34982 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+360.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 35982 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223744 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+370.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 36981 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+380.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 37981 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+390.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 38981 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+400.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 39981 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+410.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 40981 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223744 134554877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+420.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 41982 19 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+430.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 42982 20 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+440.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5815 0 0 0 43982 20 0 0 25 0 1 0 415990886 25604096 5742 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5742 603 41 0 6210 0 vsize: 25004 [startup+450.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5817 0 0 0 44982 20 0 0 25 0 1 0 415990886 25604096 5744 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5744 603 41 0 6210 0 vsize: 25004 [startup+460.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5817 0 0 0 45982 20 0 0 25 0 1 0 415990886 25604096 5744 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5744 603 41 0 6210 0 vsize: 25004 [startup+470.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5817 0 0 0 46982 20 0 0 25 0 1 0 415990886 25604096 5744 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5744 603 41 0 6210 0 vsize: 25004 [startup+480.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5817 0 0 0 47983 20 0 0 25 0 1 0 415990886 25604096 5744 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5744 603 41 0 6210 0 vsize: 25004 [startup+490.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 48983 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+500.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 49983 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+510.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 50983 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+520.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 51983 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223744 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+530.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 52983 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+540.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 53984 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223776 134560566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+550.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 54984 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+560.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 55984 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+570.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 56984 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+580.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 57984 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+590.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 58985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+600.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 59985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223824 134558330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+610.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 60985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+620.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 61985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+630.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 62985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+640.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 63985 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223744 134560194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+650.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 64986 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223796 134561241 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+660.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 65986 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+670.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5818 0 0 0 66986 20 0 0 25 0 1 0 415990886 25604096 5745 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5745 603 41 0 6210 0 vsize: 25004 [startup+680.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5819 0 0 0 67986 20 0 0 25 0 1 0 415990886 25604096 5746 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5746 603 41 0 6210 0 vsize: 25004 [startup+690.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5819 0 0 0 68986 20 0 0 25 0 1 0 415990886 25604096 5746 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5746 603 41 0 6210 0 vsize: 25004 [startup+700.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5819 0 0 0 69987 20 0 0 25 0 1 0 415990886 25604096 5746 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5746 603 41 0 6210 0 vsize: 25004 [startup+710.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5821 0 0 0 70987 20 0 0 25 0 1 0 415990886 25604096 5748 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5748 603 41 0 6210 0 vsize: 25004 [startup+720.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5822 0 0 0 71987 20 0 0 25 0 1 0 415990886 25604096 5749 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5749 603 41 0 6210 0 vsize: 25004 [startup+730.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5823 0 0 0 72987 20 0 0 25 0 1 0 415990886 25604096 5750 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5750 603 41 0 6210 0 vsize: 25004 [startup+740.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5825 0 0 0 73987 20 0 0 25 0 1 0 415990886 25604096 5752 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5752 603 41 0 6210 0 vsize: 25004 [startup+750.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 74988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221222272 134565737 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+760.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 75988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223776 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+770.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 76988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+780.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 77988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+790.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 78988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+800.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 79988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+810.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 80988 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+820.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 81989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+830.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 82989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+840.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 83989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+850.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 84989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+860.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 85989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+870.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 86989 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+880.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 87990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+890.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 88990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+900.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 89990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+910.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 90990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+920.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 91990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560276 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+930.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 92990 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+940.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 93991 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+950.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 94991 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+960.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 95991 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+970.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 96991 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560361 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+980.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 97991 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560287 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+990.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 98992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223764 134566062 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 99992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1010.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 100992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1020.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 101992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1030.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 102992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223776 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1040.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 103992 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1050.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 104993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560303 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1060.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 105993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1070.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 106993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1080.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 107993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1090.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 108993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223744 134560031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1100.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5827 0 0 0 109993 20 0 0 25 0 1 0 415990886 25604096 5754 4294967295 134512640 134672761 3221224640 3221223808 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5754 603 41 0 6210 0 vsize: 25004 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5832 0 0 0 110994 20 0 0 25 0 1 0 415990886 25604096 5759 4294967295 134512640 134672761 3221224640 3221223808 134560842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6251 5759 603 41 0 6210 0 vsize: 25004 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 5968 0 0 0 111994 21 0 0 25 0 1 0 415990886 26263552 5895 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6412 5895 603 41 0 6371 0 vsize: 25648 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6101 0 0 0 112993 21 0 0 25 0 1 0 415990886 26791936 6028 4294967295 134512640 134672761 3221224640 3221223808 134561021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6541 6028 603 41 0 6500 0 vsize: 26164 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6212 0 0 0 113993 22 0 0 25 0 1 0 415990886 27193344 6139 4294967295 134512640 134672761 3221224640 3221223744 134559949 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6639 6139 603 41 0 6598 0 vsize: 26556 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6307 0 0 0 114993 22 0 0 25 0 1 0 415990886 27586560 6234 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6735 6234 603 41 0 6694 0 vsize: 26940 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6357 0 0 0 115993 22 0 0 25 0 1 0 415990886 27852800 6284 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6800 6284 603 41 0 6759 0 vsize: 27200 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6363 0 0 0 116993 22 0 0 25 0 1 0 415990886 27852800 6290 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6800 6290 603 41 0 6759 0 vsize: 27200 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6372 0 0 0 117993 22 0 0 25 0 1 0 415990886 27852800 6299 4294967295 134512640 134672761 3221224640 3221223808 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6800 6299 603 41 0 6759 0 vsize: 27200 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6374 0 0 0 118993 22 0 0 25 0 1 0 415990886 27992064 6301 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6834 6301 603 41 0 6793 0 vsize: 27336 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5985 Raw data (stat): 5985 (minisat+) R 5984 26667 26666 0 -1 0 6377 0 0 0 119994 22 0 0 25 0 1 0 415990886 27992064 6304 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6834 6304 603 41 0 6793 0 vsize: 27336 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 5985 Raw data (stat): 5985 (minisat+) Z 5984 26667 26666 0 -1 12 6380 0 0 0 119994 24 0 0 25 0 1 0 415990886 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.05 CPU time (s): 1200.18 CPU user time (s): 1199.94 CPU system time (s): 0.241963 CPU usage (%): 100.011 Max. virtual memory (Kb): 27336 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####