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 wulflinc26 THE 2005-05-27 06:12:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23151 boxname=wulflinc26 idbench=397 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ff4eb45c2603a47e5b79b2649e926ba4 /oldhome/oroussel/tmp/wulflinc26/normalized-p0201.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc26/normalized-p0201.opb IDLAUNCH: 23151 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 851040 kB Buffers: 33048 kB Cached: 129736 kB SwapCached: 756 kB Active: 50164 kB Inactive: 114816 kB HighTotal: 131008 kB HighFree: 9072 kB LowTotal: 903652 kB LowFree: 841968 kB SwapTotal: 2097892 kB SwapFree: 2096400 kB Dirty: 36 kB Writeback: 0 kB Mapped: 5244 kB Slab: 13004 kB Committed_AS: 63732 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 06:33:16 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 23151 7 1229.85 152 #### 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 ---[ 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 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 16048 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.92 0.97 0.91 2/54 16044 Raw data (stat): 16044 (runsolver) R 16043 20687 20686 0 -1 64 0 0 0 0 0 0 0 0 19 0 1 0 853915181 1052672 97 4294967295 134512640 135381576 3221224480 3221219920 134514522 0 0 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 97 215 215 0 42 0 vsize: 1028 [startup+10 s] Raw data (loadavg): 0.93 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0004 s] Raw data (loadavg): 0.94 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0008 s] Raw data (loadavg): 0.95 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0017 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0024 s] Raw data (loadavg): 0.96 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0019 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0027 s] Raw data (loadavg): 0.97 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0034 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0037 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.004 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.68 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 16048 Raw data (stat): 16044 (minisat+_script) S 16043 20687 20686 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 853915181 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.68 CPU time (s): 1229.85 CPU user time (s): 1229.59 CPU system time (s): 0.25896 CPU usage (%): 100.014 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####