Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb |
MD5SUM | 4f5f6e30a602f3968daa9ca41c7da043 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2058 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 133 |
Biggest coefficient in the objective function | 128 |
Number of bits for the biggest coefficient in the objective function | 8 |
Sum of the numbers in the objective function | 9334 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1024 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 9334 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05284 |
Number of variables | 133 |
Total number of constraints | 126 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 56 |
Number of constraints which are nor clauses,nor cardinality constraints | 70 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 81 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-05-27 10:19:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23873 boxname=wulflinc30 idbench=1517 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f5f6e30a602f3968daa9ca41c7da043 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos5.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-neos5.opb IDLAUNCH: 23873 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 896044 kB Buffers: 5624 kB Cached: 113744 kB SwapCached: 720 kB Active: 17232 kB Inactive: 104276 kB HighTotal: 131008 kB HighFree: 13748 kB LowTotal: 903652 kB LowFree: 882296 kB SwapTotal: 2097892 kB SwapFree: 2096304 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5036 kB Slab: 11536 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 10:39:34 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 23873 7 1229.84 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 73 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 72]---> BDD-cost: 7 c ---[ 71]---> BDD-cost: 7 c ---[ 70]---> BDD-cost: 7 c ---[ 69]---> BDD-cost: 7 c ---[ 68]---> BDD-cost: 7 c ---[ 67]---> BDD-cost: 7 c ---[ 66]---> BDD-cost: 7 c ---[ 65]---> BDD-cost: 7 c ---[ 64]---> BDD-cost: 7 c ---[ 63]---> BDD-cost: 7 c ---[ 62]---> BDD-cost: 199 c ---[ 61]---> BDD-cost: 309 c ---[ 60]---> BDD-cost: 147 c ---[ 59]---> BDD-cost: 579 c ---[ 58]---> BDD-cost: 378 c ---[ 57]---> BDD-cost: 147 c ---[ 56]---> BDD-cost: 473 c ---[ 55]---> BDD-cost: 378 c ---[ 54]---> BDD-cost: 378 c ---[ 53]---> BDD-cost: 147 c ---[ 52]---> BDD-cost: 473 c ---[ 51]---> BDD-cost: 100 c ---[ 50]---> BDD-cost: 378 c ---[ 49]---> BDD-cost: 471 c ---[ 48]---> BDD-cost: 223 c ---[ 47]---> BDD-cost: 174 c ---[ 46]---> BDD-cost: 177 c ---[ 45]---> BDD-cost: 129 c ---[ 44]---> BDD-cost: 176 c ---[ 43]---> BDD-cost: 177 c ---[ 42]---> BDD-cost: 129 c ---[ 41]---> BDD-cost: 176 c ---[ 40]---> BDD-cost: 171 c ---[ 39]---> BDD-cost: 129 c ---[ 38]---> BDD-cost: 446 c ---[ 37]---> BDD-cost: 176 c ---[ 36]---> BDD-cost: 177 c ---[ 35]---> BDD-cost: 129 c ---[ 34]---> BDD-cost: 176 c ---[ 33]---> BDD-cost: 129 c ---[ 32]---> BDD-cost: 446 c ---[ 31]---> BDD-cost: 177 c ---[ 30]---> BDD-cost: 129 c ---[ 29]---> BDD-cost: 173 c ---[ 28]---> BDD-cost: 354 c ---[ 27]---> BDD-cost: 446 c ---[ 26]---> BDD-cost: 110 c ---[ 25]---> BDD-cost: 110 c ---[ 24]---> BDD-cost: 110 c ---[ 23]---> BDD-cost: 150 c ---[ 22]---> BDD-cost: 110 c ---[ 21]---> BDD-cost: 110 c ---[ 20]---> BDD-cost: 110 c ---[ 19]---> BDD-cost: 150 c ---[ 18]---> BDD-cost: 175 c ---[ 17]---> BDD-cost: 110 c ---[ 16]---> BDD-cost: 110 c ---[ 15]---> BDD-cost: 150 c ---[ 14]---> BDD-cost: 110 c ---[ 13]---> BDD-cost: 150 c ---[ 12]---> BDD-cost: 110 c ---[ 11]---> BDD-cost: 328 c ---[ 10]---> BDD-cost: 90 c ---[ 9]---> BDD-cost: 90 c ---[ 8]---> BDD-cost: 90 c ---[ 7]---> BDD-cost: 175 c ---[ 6]---> BDD-cost: 90 c ---[ 5]---> BDD-cost: 122 c ---[ 4]---> BDD-cost: 90 c ---[ 3]---> BDD-cost: 69 c ---[ 2]---> BDD-cost: 181 c ---[ 1]---> BDD-cost: 193 c ---[ 0]---> BDD-cost: 147 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 33911 100622 | 11303 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 3713[0m c ---[ 0]---> Sorter-cost: 2729 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 38898 112283 | 12966 0 0 nan | 0.000 % | c | 100 | 38898 112283 | 14262 100 915 9.2 | 0.492 % | c ============================================================================== c [1mFound solution: 2710[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 216 | 38991 112524 | 12997 216 1659 7.7 | 0.492 % | c | 317 | 38991 112524 | 14296 317 2305 7.3 | 0.497 % | c ============================================================================== c [1mFound solution: 2578[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 431 | 39004 112564 | 13001 431 3130 7.3 | 0.497 % | c | 531 | 39004 112564 | 14301 531 4162 7.8 | 0.503 % | c ============================================================================== c [1mFound solution: 2558[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 674 | 39012 112582 | 13004 674 5947 8.8 | 0.503 % | c | 774 | 39012 112582 | 14304 774 7065 9.1 | 0.510 % | c | 924 | 39012 112582 | 15734 924 8684 9.4 | 0.510 % | c | 1149 | 39012 112582 | 17308 1149 11311 9.8 | 0.510 % | c | 1487 | 39012 112582 | 19039 1487 16005 10.8 | 0.510 % | c | 1993 | 39012 112582 | 20943 1993 22485 11.3 | 0.510 % | c | 2754 | 39012 112582 | 23037 2754 32826 11.9 | 0.510 % | c ============================================================================== c [1mFound solution: 2534[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3128 | 39033 112638 | 13011 3128 38552 12.3 | 0.510 % | c | 3229 | 39033 112638 | 14312 3229 39501 12.2 | 0.516 % | c | 3379 | 39033 112638 | 15743 3379 40724 12.1 | 0.516 % | c | 3605 | 39033 112638 | 17317 3605 46529 12.9 | 0.516 % | c | 3942 | 39033 112638 | 19049 3942 51933 13.2 | 0.516 % | c | 4449 | 39033 112638 | 20954 4449 58341 13.1 | 0.516 % | c ============================================================================== c [1mFound solution: 2277[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4742 | 39062 112717 | 13020 4742 62046 13.1 | 0.516 % | c | 4842 | 39062 112717 | 14322 4842 63099 13.0 | 0.522 % | c | 4993 | 39062 112717 | 15754 4993 64889 13.0 | 0.522 % | c | 5221 | 39062 112717 | 17329 5221 67757 13.0 | 0.522 % | c | 5560 | 39062 112717 | 19062 5560 71459 12.9 | 0.522 % | c | 6067 | 39062 112717 | 20968 6067 80605 13.3 | 0.522 % | c ============================================================================== c [1mFound solution: 2226[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6796 | 39070 112741 | 13023 6796 88271 13.0 | 0.522 % | c | 6898 | 39070 112741 | 14325 6898 90654 13.1 | 0.528 % | c | 7048 | 39070 112741 | 15757 7048 92973 13.2 | 0.528 % | c | 7273 | 39070 112741 | 17333 7273 95774 13.2 | 0.528 % | c | 7611 | 39070 112741 | 19066 7611 101834 13.4 | 0.528 % | c | 8118 | 39070 112741 | 20973 8118 111260 13.7 | 0.528 % | c | 8877 | 39070 112741 | 23071 8877 127946 14.4 | 0.528 % | c | 10016 | 39070 112741 | 25378 10016 153990 15.4 | 0.528 % | c ============================================================================== c [1mFound solution: 2214[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10839 | 39075 112753 | 13025 10839 168906 15.6 | 0.528 % | c | 10940 | 39075 112753 | 14327 10940 172014 15.7 | 0.535 % | c | 11090 | 39075 112753 | 15760 11090 176255 15.9 | 0.535 % | c | 11315 | 39075 112753 | 17336 11315 180028 15.9 | 0.535 % | c | 11653 | 39075 112753 | 19069 11653 185458 15.9 | 0.535 % | c | 12160 | 39075 112753 | 20976 12160 201326 16.6 | 0.535 % | c | 12920 | 39075 112753 | 23074 12920 219136 17.0 | 0.535 % | c | 14059 | 39075 112753 | 25382 14059 250319 17.8 | 0.535 % | c | 15769 | 39075 112753 | 27920 15769 295387 18.7 | 0.535 % | c | 18331 | 39075 112753 | 30712 18331 382998 20.9 | 0.535 % | c ============================================================================== c [1mFound solution: 2198[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18608 | 39081 112766 | 13027 18608 389598 20.9 | 0.535 % | c | 18708 | 39081 112766 | 14329 9404 219670 23.4 | 0.541 % | c | 18859 | 39081 112766 | 15762 9555 222889 23.3 | 0.541 % | c | 19085 | 39081 112766 | 17338 9781 228854 23.4 | 0.541 % | c | 19423 | 39081 112766 | 19072 10119 239796 23.7 | 0.541 % | c | 19929 | 39081 112766 | 20980 10625 256430 24.1 | 0.541 % | c | 20689 | 39081 112766 | 23078 11385 273717 24.0 | 0.541 % | c | 21828 | 39081 112766 | 25385 12524 308011 24.6 | 0.541 % | c | 23536 | 39081 112766 | 27924 14232 329831 23.2 | 0.541 % | c | 26098 | 39081 112766 | 30716 16794 446902 26.6 | 0.541 % | c | 29944 | 39081 112766 | 33788 20640 593395 28.7 | 0.541 % | c ============================================================================== c [1mFound solution: 2197[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 33488 | 39084 112773 | 13028 24153 662202 27.4 | 0.541 % | c | 33588 | 39084 112773 | 14330 12177 326973 26.9 | 0.561 % | c | 33738 | 39084 112773 | 15763 12327 328428 26.6 | 0.561 % | c | 33964 | 39084 112773 | 17340 12553 331968 26.4 | 0.561 % | c | 34302 | 39084 112773 | 19074 12891 338602 26.3 | 0.561 % | c ============================================================================== c [1mFound solution: 2194[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 34788 | 39090 112786 | 13030 13377 355016 26.5 | 0.561 % | c | 34889 | 39090 112786 | 14333 6790 105552 15.5 | 0.567 % | c | 35039 | 39090 112786 | 15766 6940 109010 15.7 | 0.567 % | c | 35264 | 39090 112786 | 17342 7165 112498 15.7 | 0.567 % | c | 35602 | 39090 112786 | 19077 7503 123086 16.4 | 0.567 % | c | 36109 | 39090 112786 | 20984 8010 133240 16.6 | 0.567 % | c | 36868 | 39090 112786 | 23083 8769 151960 17.3 | 0.567 % | c | 38007 | 39090 112786 | 25391 9908 173908 17.6 | 0.567 % | c ============================================================================== c [1mFound solution: 2182[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39387 | 39095 112797 | 13031 11288 199430 17.7 | 0.567 % | c | 39488 | 39095 112797 | 14334 11389 201112 17.7 | 0.574 % | c | 39638 | 39095 112797 | 15767 11539 203455 17.6 | 0.574 % | c | 39863 | 39095 112797 | 17344 11764 206157 17.5 | 0.574 % | c | 40200 | 39095 112797 | 19078 12101 213060 17.6 | 0.574 % | c | 40707 | 39095 112797 | 20986 12608 221599 17.6 | 0.574 % | c ============================================================================== c [1mFound solution: 2181[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 41064 | 39100 112808 | 13033 12965 225861 17.4 | 0.574 % | c | 41164 | 39100 112808 | 14336 13065 228032 17.5 | 0.580 % | c | 41315 | 39100 112808 | 15769 13216 229867 17.4 | 0.580 % | c | 41540 | 39100 112808 | 17346 13441 232162 17.3 | 0.580 % | c | 41879 | 39100 112808 | 19081 13780 239794 17.4 | 0.580 % | c | 42385 | 39100 112808 | 20989 14286 250802 17.6 | 0.580 % | c ============================================================================== c [1mFound solution: 2180[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 42464 | 39110 112835 | 13036 14365 251613 17.5 | 0.580 % | c | 42564 | 39110 112835 | 14339 7283 94911 13.0 | 0.587 % | c | 42714 | 39110 112835 | 15773 7433 97580 13.1 | 0.587 % | c ============================================================================== c [1mFound solution: 2179[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 42773 | 39117 112851 | 13039 7492 98398 13.1 | 0.587 % | c | 42873 | 39117 112851 | 14342 7592 100096 13.2 | 0.593 % | c | 43023 | 39117 112851 | 15777 7742 103512 13.4 | 0.593 % | c | 43249 | 39117 112851 | 17354 7968 106173 13.3 | 0.593 % | c | 43587 | 39117 112851 | 19090 8306 111505 13.4 | 0.593 % | c | 44093 | 39117 112851 | 20999 8812 127245 14.4 | 0.593 % | c | 44852 | 39117 112851 | 23099 9571 140492 14.7 | 0.593 % | c ============================================================================== c [1mFound solution: 2178[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45190 | 39124 112867 | 13041 9909 145231 14.7 | 0.593 % | c | 45290 | 39124 112867 | 14345 10009 146867 14.7 | 0.600 % | c | 45441 | 39124 112867 | 15779 10160 150101 14.8 | 0.600 % | c | 45666 | 39124 112867 | 17357 10385 153677 14.8 | 0.600 % | c | 46004 | 39124 112867 | 19093 10723 160889 15.0 | 0.600 % | c | 46510 | 39124 112867 | 21002 11229 172904 15.4 | 0.600 % | c | 47270 | 39124 112867 | 23102 11989 194129 16.2 | 0.600 % | c | 48409 | 39124 112867 | 25413 13128 230083 17.5 | 0.600 % | c | 50117 | 39124 112867 | 27954 14836 265720 17.9 | 0.600 % | c ============================================================================== c [1mFound solution: 2118[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51555 | 39133 112892 | 13044 16274 329483 20.2 | 0.600 % | c | 51656 | 39133 112892 | 14348 8238 177098 21.5 | 0.606 % | c | 51806 | 39133 112892 | 15783 8388 180206 21.5 | 0.606 % | c | 52032 | 39133 112892 | 17361 8614 184942 21.5 | 0.606 % | c | 52370 | 39133 112892 | 19097 8952 190096 21.2 | 0.606 % | c | 52876 | 39133 112892 | 21007 9458 198770 21.0 | 0.606 % | c | 53635 | 39133 112892 | 23108 10217 223410 21.9 | 0.606 % | c | 54774 | 39133 112892 | 25419 11356 239738 21.1 | 0.606 % | c | 56483 | 39133 112892 | 27960 13065 277316 21.2 | 0.606 % | c | 59045 | 39133 112892 | 30757 15627 356100 22.8 | 0.606 % | c | 62891 | 39133 112892 | 33832 19473 448248 23.0 | 0.606 % | c ============================================================================== c [1mFound solution: 2113[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 63186 | 39140 112908 | 13046 19768 453358 22.9 | 0.606 % | c | 63286 | 39140 112908 | 14350 9984 197679 19.8 | 0.613 % | c | 63436 | 39140 112908 | 15785 10134 201781 19.9 | 0.613 % | c | 63661 | 39140 112908 | 17364 10359 205325 19.8 | 0.613 % | c | 63998 | 39140 112908 | 19100 10696 210724 19.7 | 0.613 % | c | 64507 | 39140 112908 | 21010 11205 228279 20.4 | 0.613 % | c | 65266 | 39140 112908 | 23111 11964 241822 20.2 | 0.613 % | c | 66410 | 39140 112908 | 25422 13108 269151 20.5 | 0.613 % | c | 68119 | 39140 112908 | 27965 14817 326657 22.0 | 0.613 % | c | 70681 | 39140 112908 | 30761 17379 373421 21.5 | 0.613 % | c | 74525 | 39140 112908 | 33837 21223 458843 21.6 | 0.613 % | c | 80292 | 39140 112908 | 37221 26990 707568 26.2 | 0.613 % | c | 88941 | 39140 112908 | 40943 35639 1070103 30.0 | 0.613 % | c ============================================================================== c [1mFound solution: 2108[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 91101 | 39149 112929 | 13049 37799 1190486 31.5 | 0.613 % | c | 91201 | 39149 112929 | 14353 7733 232503 30.1 | 0.619 % | c | 91351 | 39147 112925 | 15789 7881 233984 29.7 | 0.626 % | c | 91576 | 39147 112925 | 17368 8106 237486 29.3 | 0.626 % | c | 91913 | 39147 112925 | 19105 8443 244004 28.9 | 0.626 % | c | 92421 | 39147 112925 | 21015 8951 252559 28.2 | 0.626 % | c | 93180 | 39147 112925 | 23117 9710 265335 27.3 | 0.626 % | c | 94321 | 39147 112925 | 25428 10851 286293 26.4 | 0.626 % | c | 96031 | 39147 112925 | 27971 12561 324430 25.8 | 0.626 % | c | 98595 | 39147 112925 | 30768 15125 381915 25.3 | 0.626 % | c ============================================================================== c [1mFound solution: 2086[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 99390 | 39152 112936 | 13050 15920 392230 24.6 | 0.626 % | c | 99490 | 39152 112936 | 14355 8060 123820 15.4 | 0.632 % | c | 99641 | 39152 112936 | 15790 8211 126017 15.3 | 0.632 % | c | 99866 | 39152 112936 | 17369 8436 128818 15.3 | 0.632 % | c | 100203 | 39152 112936 | 19106 8773 135875 15.5 | 0.632 % | c | 100710 | 39152 112936 | 21017 9280 144258 15.5 | 0.632 % | c | 101469 | 39152 112936 | 23118 10039 157672 15.7 | 0.632 % | c | 102609 | 39152 112936 | 25430 11179 178631 16.0 | 0.632 % | c ============================================================================== c [1mFound solution: 2084[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104126 | 39159 112952 | 13053 12696 214227 16.9 | 0.632 % | c | 104226 | 39159 112952 | 14358 12796 218101 17.0 | 0.638 % | c | 104379 | 39159 112952 | 15794 12949 221494 17.1 | 0.638 % | c | 104604 | 39159 112952 | 17373 13174 225818 17.1 | 0.638 % | c | 104942 | 39159 112952 | 19110 13512 230644 17.1 | 0.638 % | c | 105448 | 39159 112952 | 21021 14018 237233 16.9 | 0.638 % | c | 106207 | 39159 112952 | 23124 14777 251872 17.0 | 0.638 % | c | 107346 | 39159 112952 | 25436 15916 284816 17.9 | 0.638 % | c ============================================================================== c [1mFound solution: 2054[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 108040 | 39164 112963 | 13054 16610 296982 17.9 | 0.638 % | c | 108140 | 39164 112963 | 14359 8405 125008 14.9 | 0.645 % | c | 108291 | 39164 112963 | 15795 8556 128637 15.0 | 0.645 % | c | 108516 | 39164 112963 | 17374 8781 134950 15.4 | 0.645 % | c | 108855 | 39164 112963 | 19112 9120 141445 15.5 | 0.645 % | c | 109363 | 39164 112963 | 21023 9628 154186 16.0 | 0.645 % | c | 110122 | 39164 112963 | 23125 10387 168963 16.3 | 0.645 % | c | 111261 | 39164 112963 | 25438 11526 199481 17.3 | 0.645 % | c ============================================================================== c [1mFound solution: 2053[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112223 | 39170 112976 | 13056 12488 218124 17.5 | 0.645 % | c | 112323 | 39170 112976 | 14361 12588 220064 17.5 | 0.651 % | c | 112473 | 39170 112976 | 15797 12738 222376 17.5 | 0.651 % | c ============================================================================== c [1mFound solution: 2052[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 112587 | 39176 112989 | 13058 12852 224961 17.5 | 0.651 % | c | 112688 | 39176 112989 | 14363 12953 227121 17.5 | 0.658 % | c | 112838 | 39176 112989 | 15800 13103 231056 17.6 | 0.658 % | c | 113063 | 39176 112989 | 17380 13328 236720 17.8 | 0.658 % | c | 113401 | 39176 112989 | 19118 13666 242970 17.8 | 0.658 % | c | 113908 | 39176 112989 | 21030 14173 248818 17.6 | 0.658 % | c | 114668 | 39176 112989 | 23133 14933 259678 17.4 | 0.658 % | c ============================================================================== c [1mFound solution: 2051[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115732 | 39183 113004 | 13061 15997 300594 18.8 | 0.658 % | c | 115832 | 39183 113004 | 14367 8099 119026 14.7 | 0.664 % | c | 115982 | 39183 113004 | 15803 8249 121516 14.7 | 0.664 % | c | 116208 | 39183 113004 | 17384 8475 125658 14.8 | 0.664 % | c | 116545 | 39183 113004 | 19122 8812 134437 15.3 | 0.664 % | c | 117051 | 39183 113004 | 21034 9318 144441 15.5 | 0.664 % | c | 117810 | 39183 113004 | 23138 10077 158441 15.7 | 0.664 % | c | 118949 | 39183 113004 | 25452 11216 177286 15.8 | 0.664 % | c | 120657 | 39183 113004 | 27997 12924 222332 17.2 | 0.664 % | c ============================================================================== c [1mFound solution: 2050[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 122005 | 39190 113019 | 13063 14272 264416 18.5 | 0.664 % | c | 122105 | 39190 113019 | 14369 7236 118286 16.3 | 0.671 % | c | 122255 | 39190 113019 | 15806 7386 120790 16.4 | 0.671 % | c | 122480 | 39190 113019 | 17386 7611 124288 16.3 | 0.671 % | c | 122818 | 39190 113019 | 19125 7949 127889 16.1 | 0.671 % | c | 123325 | 39190 113019 | 21038 8456 136221 16.1 | 0.671 % | c | 124086 | 39190 113019 | 23141 9217 163643 17.8 | 0.671 % | c | 125225 | 39190 113019 | 25456 10356 191362 18.5 | 0.671 % | c | 126933 | 39190 113019 | 28001 12064 237174 19.7 | 0.671 % | c | 129495 | 39187 113012 | 30801 14509 347040 23.9 | 0.684 % | c | 133343 | 39187 113012 | 33882 18357 531606 29.0 | 0.684 % | c | 139109 | 39187 113012 | 37270 24123 755871 31.3 | 0.684 % | c ============================================================================== c [1mFound solution: 2049[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 144688 | 39192 113023 | 13064 29702 944308 31.8 | 0.684 % | c | 144788 | 39192 113023 | 14370 7526 155241 20.6 | 0.690 % | c | 144940 | 39192 113023 | 15807 7678 157505 20.5 | 0.690 % | c | 145165 | 39192 113023 | 17388 7903 162421 20.6 | 0.690 % | c | 145503 | 39192 113023 | 19127 8241 168934 20.5 | 0.690 % | c | 146013 | 39192 113023 | 21039 8751 179552 20.5 | 0.690 % | c | 146774 | 39192 113023 | 23143 9512 190278 20.0 | 0.690 % | c | 147913 | 39190 113019 | 25458 10650 219684 20.6 | 0.697 % | c | 149622 | 39190 113019 | 28003 12359 257758 20.9 | 0.697 % | c | 152184 | 39190 113019 | 30804 14921 332505 22.3 | 0.697 % | c | 156030 | 39190 113019 | 33884 18767 416429 22.2 | 0.697 % | c | 161797 | 39190 113019 | 37273 24534 516462 21.1 | 0.697 % | c ============================================================================== c [1mFound solution: 2048[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 164737 | 39199 113039 | 13066 27474 601402 21.9 | 0.697 % | c | 164837 | 39199 113039 | 14372 6969 110704 15.9 | 0.703 % | c | 164989 | 39199 113039 | 15809 7121 112243 15.8 | 0.703 % | c | 165214 | 39199 113039 | 17390 7346 116712 15.9 | 0.703 % | c | 165551 | 39199 113039 | 19129 7683 124270 16.2 | 0.703 % | c | 166058 | 39199 113039 | 21042 8190 131152 16.0 | 0.703 % | c | 166817 | 39199 113039 | 23147 8949 146515 16.4 | 0.703 % | c | 167956 | 39199 113039 | 25461 10088 173923 17.2 | 0.703 % | c | 169665 | 39199 113039 | 28008 11797 221617 18.8 | 0.703 % | c | 172227 | 39199 113039 | 30808 14359 304218 21.2 | 0.703 % | c | 176071 | 39199 113039 | 33889 18203 409817 22.5 | 0.703 % | c | 181838 | 39199 113039 | 37278 23970 535018 22.3 | 0.703 % | c | 190487 | 39199 113039 | 41006 32619 809512 24.8 | 0.703 % | c | 203461 | 39199 113039 | 45107 19849 514697 25.9 | 0.703 % | c ============================================================================== c [1mFound solution: 2022[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 219104 | 39215 113080 | 13071 35492 1638422 46.2 | 0.703 % | c | 219206 | 39215 113080 | 14378 7685 342507 44.6 | 0.709 % | c | 219356 | 39215 113080 | 15815 7835 345471 44.1 | 0.709 % | c | 219584 | 39215 113080 | 17397 8063 348088 43.2 | 0.709 % | c | 219922 | 39215 113080 | 19137 8401 357441 42.5 | 0.709 % | c | 220428 | 39215 113080 | 21050 8907 366831 41.2 | 0.709 % | c | 221187 | 39215 113080 | 23156 9666 380360 39.4 | 0.709 % | c | 222326 | 39215 113080 | 25471 10805 400433 37.1 | 0.709 % | c | 224035 | 39215 113080 | 28018 12514 458854 36.7 | 0.709 % | c | 226597 | 39215 113080 | 30820 15076 511688 33.9 | 0.709 % | c | 230442 | 39215 113080 | 33902 18921 595632 31.5 | 0.709 % | c | 236208 | 39215 113080 | 37293 24687 716653 29.0 | 0.709 % | c | 244857 | 39215 113080 | 41022 33336 956691 28.7 | 0.709 % | c | 257832 | 39215 113080 | 45124 19491 624862 32.1 | 0.709 % | c | 277293 | 39215 113080 | 49637 38952 1587769 40.8 | 0.709 % | c | 306485 | 39215 113080 | 54600 32539 847118 26.0 | 0.709 % | c ============================================================================== c [1mFound solution: 2020[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 345044 | 39220 113096 | 13073 30496 1280501 42.0 | 0.709 % | c | 345144 | 39220 113096 | 14380 7724 164218 21.3 | 0.716 % | c | 345295 | 39220 113096 | 15818 7875 166112 21.1 | 0.716 % | c | 345520 | 39220 113096 | 17400 8100 170123 21.0 | 0.716 % | c | 345859 | 39220 113096 | 19140 8439 174731 20.7 | 0.716 % | c | 346366 | 39220 113096 | 21054 8946 182386 20.4 | 0.716 % | c | 347130 | 39215 113085 | 23159 9698 199767 20.6 | 0.735 % | c | 348273 | 39215 113085 | 25475 10841 221330 20.4 | 0.735 % | c | 349981 | 39215 113085 | 28023 12549 255128 20.3 | 0.735 % | c | 352545 | 39215 113085 | 30825 15113 305897 20.2 | 0.735 % | c | 356389 | 39215 113085 | 33907 18957 380955 20.1 | 0.735 % | c | 362155 | 39215 113085 | 37298 24723 543954 22.0 | 0.735 % | c | 370804 | 39215 113085 | 41028 33372 690051 20.7 | 0.735 % | c | 383778 | 39215 113085 | 45131 20751 703195 33.9 | 0.735 % | c | 403239 | 39215 113085 | 49644 40212 1938012 48.2 | 0.735 % | c ============================================================================== c [1mFound solution: 2019[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 413668 | 39221 113100 | 13073 18494 529233 28.6 | 0.735 % | c | 413768 | 39221 113100 | 14380 9347 209360 22.4 | 0.742 % | c | 413919 | 39221 113100 | 15818 9498 211857 22.3 | 0.742 % | c | 414144 | 39221 113100 | 17400 9723 215991 22.2 | 0.742 % | c | 414481 | 39221 113100 | 19140 10060 221556 22.0 | 0.742 % | c | 414987 | 39221 113100 | 21054 10566 230833 21.8 | 0.742 % | c | 415747 | 39221 113100 | 23159 11326 248579 21.9 | 0.742 % | c | 416886 | 39221 113100 | 25475 12465 268279 21.5 | 0.742 % | c | 418596 | 39221 113100 | 28023 14175 303062 21.4 | 0.742 % | c | 421160 | 39221 113100 | 30825 16739 374019 22.3 | 0.742 % | c | 425005 | 39221 113100 | 33907 20584 457277 22.2 | 0.742 % | c | 430772 | 39221 113100 | 37298 26351 554524 21.0 | 0.742 % | c | 439421 | 39221 113100 | 41028 35000 1026168 29.3 | 0.742 % | c | 452396 | 39221 113100 | 45131 22551 990398 43.9 | 0.742 % | c | 471857 | 39221 113100 | 49644 42012 2141032 51.0 | 0.742 % | c | 501049 | 39221 113100 | 54609 35709 1166547 32.7 | 0.742 % | c ============================================================================== c [1mFound solution: 2018[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 516644 | 39227 113115 | 13075 51304 2106940 41.1 | 0.742 % | c | 516744 | 39227 113115 | 14382 8377 255250 30.5 | 0.748 % | c | 516895 | 39227 113115 | 15820 8528 258995 30.4 | 0.748 % | c | 517124 | 39227 113115 | 17402 8757 265447 30.3 | 0.748 % | c | 517461 | 39227 113115 | 19143 9094 272822 30.0 | 0.748 % | c | 517969 | 39227 113115 | 21057 9602 284892 29.7 | 0.748 % | c | 518729 | 39227 113115 | 23163 10362 299097 28.9 | 0.748 % | c | 519869 | 39227 113115 | 25479 11502 336446 29.3 | 0.748 % | c | 521578 | 39227 113115 | 28027 13211 387412 29.3 | 0.748 % | c | 524141 | 39227 113115 | 30830 15774 452571 28.7 | 0.748 % | c | 527987 | 39227 113115 | 33913 19620 556397 28.4 | 0.748 % | c | 533753 | 39227 113115 | 37304 25386 762984 30.1 | 0.748 % | c | 542402 | 39227 113115 | 41034 34035 1081862 31.8 | 0.748 % | c ============================================================================== c [1mFound solution: 2017[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 549661 | 39233 113130 | 13077 41294 1270505 30.8 | 0.748 % | c | 549761 | 39233 113130 | 14384 8570 124264 14.5 | 0.754 % | c | 549911 | 39233 113130 | 15823 8720 126840 14.5 | 0.754 % | c | 550136 | 39233 113130 | 17405 8945 130346 14.6 | 0.754 % | c | 550473 | 39233 113130 | 19146 9282 136791 14.7 | 0.754 % | c | 550983 | 39233 113130 | 21060 9792 150415 15.4 | 0.754 % | c | 551742 | 39233 113130 | 23166 10551 166685 15.8 | 0.754 % | c | 552881 | 39233 113130 | 25483 11690 182816 15.6 | 0.754 % | c | 554591 | 39233 113130 | 28031 13400 227750 17.0 | 0.754 % | c | 557154 | 39233 113130 | 30834 15963 292954 18.4 | 0.754 % | c | 560998 | 39233 113130 | 33918 19807 385678 19.5 | 0.754 % | c | 566766 | 39233 113130 | 37310 25575 528204 20.7 | 0.754 % | c | 575415 | 39233 113130 | 41041 34224 909593 26.6 | 0.754 % | c | 588389 | 39233 113130 | 45145 18961 528667 27.9 | 0.754 % | c | 607851 | 39233 113130 | 49659 38423 1022299 26.6 | 0.755 % | c | 637044 | 39233 113130 | 54625 34500 1479658 42.9 | 0.754 % | c | 680833 | 39233 113130 | 60088 38207 1141570 29.9 | 0.755 % | c ============================================================================== c [1mFound solution: 2016[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 712040 | 39239 113145 | 13079 23500 914500 38.9 | 0.755 % | c | 712140 | 39239 113145 | 14386 11850 577102 48.7 | 0.761 % | c | 712290 | 39239 113145 | 15825 12000 579032 48.3 | 0.761 % | c | 712516 | 39239 113145 | 17408 12226 583747 47.7 | 0.761 % | c | 712854 | 39239 113145 | 19148 12564 589558 46.9 | 0.761 % | c | 713360 | 39239 113145 | 21063 13070 605699 46.3 | 0.761 % | c | 714120 | 39239 113145 | 23170 13830 625085 45.2 | 0.761 % | c | 715259 | 39239 113145 | 25487 14969 655852 43.8 | 0.761 % | c | 716967 | 39239 113145 | 28035 16677 708245 42.5 | 0.761 % | c | 719531 | 39239 113145 | 30839 19241 786345 40.9 | 0.761 % | c | 723375 | 39239 113145 | 33923 23085 932446 40.4 | 0.761 % | c | 729141 | 39239 113145 | 37315 28851 1125574 39.0 | 0.761 % | c ============================================================================== c [1mFound solution: 2006[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 736188 | 39245 113159 | 13081 35898 1371377 38.2 | 0.761 % | c | 736288 | 39245 113159 | 14389 8356 107806 12.9 | 0.767 % | c | 736438 | 39245 113159 | 15828 8506 110493 13.0 | 0.767 % | c | 736664 | 39245 113159 | 17410 8732 114630 13.1 | 0.767 % | c | 737003 | 39245 113159 | 19151 9071 119717 13.2 | 0.767 % | c | 737510 | 39245 113159 | 21067 9578 129395 13.5 | 0.767 % | c | 738269 | 39245 113159 | 23173 10337 151025 14.6 | 0.767 % | c | 739408 | 39245 113159 | 25491 11476 183982 16.0 | 0.767 % | c | 741117 | 39245 113159 | 28040 13185 240450 18.2 | 0.767 % | c | 743680 | 39245 113159 | 30844 15748 321035 20.4 | 0.767 % | c ============================================================================== c [1mFound solution: 2005[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 746764 | 39251 113173 | 13083 18832 416684 22.1 | 0.767 % | c | 746864 | 39251 113173 | 14391 9516 186005 19.5 | 0.774 % | c | 747014 | 39251 113173 | 15830 9666 190248 19.7 | 0.774 % | c | 747239 | 39251 113173 | 17413 9891 196259 19.8 | 0.774 % | c | 747577 | 39251 113173 | 19154 10229 205501 20.1 | 0.774 % | c | 748083 | 39251 113173 | 21070 10735 219323 20.4 | 0.774 % | c | 748842 | 39251 113173 | 23177 11494 240973 21.0 | 0.774 % | c ============================================================================== c [1mFound solution: 1998[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 749443 | 39260 113194 | 13086 12095 263797 21.8 | 0.774 % | c | 749544 | 39260 113194 | 14394 12196 266861 21.9 | 0.780 % | c | 749695 | 39260 113194 | 15834 12347 271873 22.0 | 0.780 % | c | 749920 | 39260 113194 | 17417 12572 275432 21.9 | 0.780 % | c | 750257 | 39260 113194 | 19159 12909 279411 21.6 | 0.780 % | c | 750763 | 39260 113194 | 21075 13415 285346 21.3 | 0.780 % | c | 751522 | 39260 113194 | 23182 14174 305973 21.6 | 0.780 % | c | 752661 | 39260 113194 | 25500 15313 331679 21.7 | 0.780 % | c | 754369 | 39260 113194 | 28051 17021 360309 21.2 | 0.780 % | c | 756932 | 39260 113194 | 30856 19584 442144 22.6 | 0.780 % | c | 760778 | 39260 113194 | 33941 23430 557363 23.8 | 0.780 % | c | 766544 | 39260 113194 | 37335 29196 737982 25.3 | 0.780 % | c | 775193 | 39260 113194 | 41069 17046 406925 23.9 | 0.780 % | c ============================================================================== c [1mFound solution: 1996[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 781405 | 39269 113215 | 13089 23258 615788 26.5 | 0.780 % | c | 781505 | 39269 113215 | 14397 11729 254937 21.7 | 0.786 % | c | 781660 | 39269 113215 | 15837 11884 259362 21.8 | 0.786 % | c | 781886 | 39269 113215 | 17421 12110 266809 22.0 | 0.786 % | c | 782223 | 39269 113215 | 19163 12447 275155 22.1 | 0.786 % | c | 782729 | 39269 113215 | 21079 12953 292925 22.6 | 0.786 % | c | 783488 | 39269 113215 | 23187 13712 306853 22.4 | 0.786 % | c | 784627 | 39269 113215 | 25506 14851 340029 22.9 | 0.786 % | c | 786335 | 39269 113215 | 28057 16559 394345 23.8 | 0.786 % | c | 788899 | 39269 113215 | 30863 19123 490108 25.6 | 0.786 % | c | 792745 | 39269 113215 | 33949 22969 600146 26.1 | 0.786 % | c | 798512 | 39269 113215 | 37344 28736 819817 28.5 | 0.786 % | c | 807162 | 39269 113215 | 41078 37386 1106840 29.6 | 0.786 % | c | 820136 | 39259 113193 | 45186 26222 712569 27.2 | 0.825 % | c ============================================================================== c [1mFound solution: 1995[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 831545 | 39268 113214 | 13089 37631 1257604 33.4 | 0.825 % | c | 831646 | 39268 113214 | 14397 8371 284428 34.0 | 0.832 % | c | 831796 | 39268 113214 | 15837 8521 287306 33.7 | 0.832 % | c | 832021 | 39268 113214 | 17421 8746 292432 33.4 | 0.832 % | c | 832358 | 39268 113214 | 19163 9083 299700 33.0 | 0.832 % | c | 832865 | 39268 113214 | 21079 9590 313068 32.6 | 0.832 % | c | 833624 | 39268 113214 | 23187 10349 329581 31.8 | 0.832 % | c | 834763 | 39268 113214 | 25506 11488 356496 31.0 | 0.832 % | c | 836471 | 39268 113214 | 28057 13196 407735 30.9 | 0.832 % | c | 839034 | 39268 113214 | 30863 15759 484410 30.7 | 0.832 % | c | 842878 | 39268 113214 | 33949 19603 590220 30.1 | 0.832 % | c | 848645 | 39268 113214 | 37344 25370 777976 30.7 | 0.832 % | c ============================================================================== c [1mFound solution: 1994[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 853834 | 39277 113235 | 13092 30559 899600 29.4 | 0.832 % | c | 853935 | 39277 113235 | 14401 7741 90993 11.8 | 0.838 % | c | 854085 | 39277 113235 | 15841 7891 93905 11.9 | 0.838 % | c | 854312 | 39277 113235 | 17425 8118 100603 12.4 | 0.838 % | c | 854650 | 39277 113235 | 19167 8456 111345 13.2 | 0.838 % | c | 855158 | 39277 113235 | 21084 8964 126635 14.1 | 0.838 % | c | 855917 | 39277 113235 | 23193 9723 150345 15.5 | 0.838 % | c | 857056 | 39277 113235 | 25512 10862 187597 17.3 | 0.838 % | c | 858764 | 39277 113235 | 28063 12570 244480 19.4 | 0.838 % | c | 861326 | 39277 113235 | 30870 15132 332740 22.0 | 0.838 % | c | 865171 | 39277 113235 | 33957 18977 471211 24.8 | 0.838 % | c | 870937 | 39277 113235 | 37353 24743 656602 26.5 | 0.838 % | c | 879587 | 39277 113235 | 41088 33393 931635 27.9 | 0.838 % | c | 892561 | 39277 113235 | 45197 19566 467043 23.9 | 0.838 % | c | 912022 | 39277 113235 | 49716 39027 969843 24.9 | 0.838 % | c | 941214 | 39277 113235 | 54688 36738 982641 26.7 | 0.838 % | c | 985003 | 39277 113235 | 60157 42175 1106581 26.2 | 0.838 % | c ============================================================================== c [1mFound solution: 1993[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 995602 | 39286 113256 | 13095 52774 1721731 32.6 | 0.838 % | c | 995704 | 39286 113256 | 14404 8775 378088 43.1 | 0.844 % | c | 995856 | 39286 113256 | 15844 8927 382919 42.9 | 0.844 % | c | 996083 | 39286 113256 | 17429 9154 388160 42.4 | 0.844 % | c | 996420 | 39286 113256 | 19172 9491 397955 41.9 | 0.844 % | c | 996926 | 39286 113256 | 21089 9997 415034 41.5 | 0.844 % | c | 997685 | 39286 113256 | 23198 10756 439293 40.8 | 0.844 % | c | 998824 | 39286 113256 | 25518 11895 482514 40.6 | 0.844 % | c | 1000532 | 39286 113256 | 28070 13603 541679 39.8 | 0.844 % | c | 1003094 | 39286 113256 | 30877 16165 621066 38.4 | 0.844 % | c | 1006938 | 39286 113256 | 33965 20009 754003 37.7 | 0.844 % | c | 1012704 | 39286 113256 | 37361 25775 954909 37.0 | 0.844 % | c | 1021353 | 39286 113256 | 41097 34424 1287036 37.4 | 0.844 % | c | 1034327 | 39286 113256 | 45207 22859 732705 32.1 | 0.844 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 21409 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.85 0.95 0.91 2/54 21405 Raw data (stat): 21405 (runsolver) R 21404 22056 22055 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 855381549 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.87 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0013 s] Raw data (loadavg): 0.89 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0008 s] Raw data (loadavg): 0.91 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0009 s] Raw data (loadavg): 0.92 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0017 s] Raw data (loadavg): 0.93 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0012 s] Raw data (loadavg): 0.94 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0167 s] Raw data (loadavg): 0.95 0.95 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0261 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0266 s] Raw data (loadavg): 0.96 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.027 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.027 s] Raw data (loadavg): 0.97 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.027 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.027 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.028 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.028 s] Raw data (loadavg): 0.98 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.029 s] Raw data (loadavg): 0.99 0.96 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.031 s] Raw data (loadavg): 0.99 0.97 0.91 3/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/55 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 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 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.69 s] Raw data (loadavg): 0.99 0.97 0.91 1/53 21409 Raw data (stat): 21405 (minisat+_script) S 21404 22056 22055 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 855381549 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.69 CPU time (s): 1229.84 CPU user time (s): 1229.6 CPU system time (s): 0.244962 CPU usage (%): 100.013 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####